Planarian’s guarantees
planarian @ a924e09 · Spec v4.6 · snapshot main · all versions
What Planarian promises, and the code, proofs, tests and limits that carry each promise, computed from the repository at this commit (SPEC §17c).
25 invariants · 52 obligations discharged against 63 assumptions (d:a 52 : 63) · 29 assumptions · 39 bypass rows · 161 gym entries
| Invariant | Statement | Status | d:a | Gym | Limits |
|---|---|---|---|---|---|
| I1 | A boot-confirmed known-good generation always exists, is bootable, and is in the boot menu | Tested, not proved | 0 : 2 | 3 | 5 |
| I2 | The installed core package’s hash equals the hash recorded in its signature | Tested, not proved | 0 : 2 | 2 | 6 |
| I3 | Garbage collection never removes known-good, the previous generation, the current genera… | Tested, not proved | 0 : 2 | 3 | 5 |
| I4 | Running means desired-Running under the current conditions, observed-active, and every… | Tested, not proved | 0 : 1 | 1 | 6 |
| I5 | Forbidden actions are unrepresentable as transitions | Proved | 4 : 3 | 1 | 5 |
| I6 | At most one generation-changing transaction is active (a generation transaction waiting … | Proved | 7 : 5 | 9 | 5 |
| I7 | Every executed transition is logged with proposal, source, pre- and post-state, derived … | Tested, not proved | 0 : 1 | 0 | 5 |
| I8 | A tier-3 transition executes only with an approval token bound to the concrete candidate… | Proved | 1 : 1 | 4 | 6 |
| I9 | The model process holds exactly one write capability: submit a proposal | Neither proved nor tested | 0 : 1 | 0 | 6 |
| I10 | No change that removes or alters a canonical probe executes below AskFirst, and canonica… | Proved | 1 : 2 | 4 | 5 |
| I11 | A session’s cumulative effect is classified at least as high as any single transition pr… | Proved | 2 : 2 | 1 | 5 |
| I12 | Under the progress assumptions of §17a, every transaction in the journal reaches a termi… | Proved | 9 : 8 | 6 | 5 |
| I13 | A unit under an override is never a repair target while the override holds | Proved | 3 : 2 | 2 | 5 |
| I14 | Policy facts (sensitivity, affected units, manifest-touching, caller identity) are deriv… | Proved | 1 : 2 | 4 | 6 |
| I15 | Exactly one owner (lease) per transaction | Proved | 2 : 2 | 7 | 6 |
| I16 | No automatic revert, rollback, or boot fallback selects a generation below the security … | Proved | 2 : 3 | 5 | 6 |
| I17 | The set of principals holding administrator capability is never empty | Proved | 2 : 2 | 1 | 5 |
| I18 | Every journal record commits to the hash of its predecessor | Proved | 5 : 3 | 3 | 6 |
| I19 | No principal approves its own proposal, and no principal grants itself, or a principal i… | Proved | 3 : 3 | 3 | 5 |
| I20 | No agent (the on-device model, a remote relay, or any agent started by `planarian agent … | Tested, not proved | 0 : 2 | 7 | 8 |
| I21 | No transition that cannot be reversed, or that may lose a session, user data or connecti… | Proved | 2 : 4 | 4 | 7 |
| I22 | Changing the generation, collecting garbage, binding drivers, resolving the recovery int… | Proved | 5 : 4 | 3 | 8 |
| I23 | A generation transaction commits only after its boot entry is written and promoted | Proved | 3 : 1 | 2 | 6 |
| I24 | An agent’s authority is bound to the one AgentStarted record for the unit instance it … | Tested, not proved | 0 : 3 | 1 | 6 |
| I25 | Post-commit bookkeeping (security-floor derivation, the committed generation’s override … | Tested, not proved | 0 : 2 | 3 | 5 |