I9 · The model process holds exactly one write capability: submit a proposal

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

The model process holds exactly one write capability: submit a proposal.

— SPEC §7

Status	Proof phase	d:a	Gym
Neither proved nor tested	B (by the sandbox, §20, and a gym case), E (proof)	0 : 1 (baseline 0 : 1, not degraded)	0 entries, 0 must-pass

How it is proved

No obligation discharges it: nothing about it is proved.

If any of these is false, the proof no longer describes the real machine.

Id	Assumption	Kind	Also relied on by
P8	The kernel and systemd are correct	Platform	I1, I2, I3, I17, I20, I22

No gym entry exercises it.

Bypass	Route	Severity	Status	Closes in
B-18	The model service escapes its sandbox before I9 is proved, and becomes a process with its uid’s capabilities (it parses untrusted text and drives a GPU)	Medium	Open (v4.5 §20, I9)	B sandbox and case; E proof
X-1	Root edits the store, `/boot`, the binaries, the journal or the posture state	Accepted	Accepted	E
X-2	A `nixos-rebuild` outside Planarian	Accepted	Accepted	C
X-4	Physical access	Accepted	Accepted	E
X-6	The supply chain: nixpkgs content, cache signatures, input-addressed store paths	Accepted	Accepted	—
X-7	Backends report success falsely; systemd or the kernel misbehave (P1, P6, P8)	Accepted	Accepted	D, E

Spec	Change
v4	Restored principles (now 12) and invariants (I1–I14) that v3 referenced but omitted
v4.5	§20, I9: the model is treated as an adversary, so its judgement is not a vector