Conformance & proofs

Nine checked models, and one link that is missing.

Byom's most impressive-looking asset is its model suite: nine TLA+ modules, each explored exhaustively by TLC at its configured constants, with zero errors and crashes interleaved at every commit boundary. The honest statement about them belongs at the top of this page rather than the bottom.

The gap, stated first

No automated test connects the models to the code

No test in crates/ reads a descriptor or a TLA+ model at all. The Rust tests include_str! the schemas, the vectors, the registry and the MCP tool document — never spec/descriptors/ and never proof/specs/. The conformance oracle that would assert, for every (state, event) pair, that the daemon's pure transition functions equal the committed relations was expected to land with the daemon. The daemon landed; the oracle did not.

So: the models are checked, and they are not connected to the implementation by any automated test. A daemon transition can diverge from its committed descriptor row without anything in this repository noticing. Every model's refinement boundary below therefore stops at the descriptor, and no model on this page claims that any code refines it.

This is recorded as the single largest open item in the proof properties document, and the acceptance decision that requires it carries an erratum saying the same thing. It is written here, in the same size type as the models, because a site claiming "machine-checked protocol models" without it would be exactly the overclaim this program has spent thirty-odd corrections removing.

Five layers of checking

Each layer catches a different failure, and each is independent of the others. It is worth being precise about which one catches what, because "it is verified" is not a claim any single one of them supports.

layer 1

TLC over the models

Exhaustive breadth-first exploration at fixed constants, with -deadlock, zero errors. Catches: an invariant that a legal interleaving can break. Does not catch: a model that does not match the design, or code that does not match the model.

layer 2

Descriptor ↔ model parity

Exact set equality in both directions over states and transitions, plus the structured crash and fence columns. Catches: a descriptor row with no model transition, or a model transition with no row. Does not catch: an edited TLA+ action whose annotation and descriptor were left alone.

layer 3

Executable state walks

Vectors driven through an interpreter over the committed descriptor JSON, independent of both TLC and the parity checker. Catches: a machine whose committed rows do not actually admit the sequence they are supposed to — including crash and replay steps.

layer 4

The mutation suite

Deliberate damage that must be caught. Catches: a vacuous harness — a gate that passes because it is checking nothing. This is the layer that makes the other layers' green mean something.

layer 5

Independent rederivation

Every canonical byte and digest the family profile pins, re-derived by two programs sharing no code with the workspace or with each other. Catches: a canonicalization or digest bug that the implementation and its own tests agree on.

the missing layer

Model ↔ code conformance

A test asserting that the daemon's transition functions equal the committed relations, generated from the descriptor registry rather than re-typed. It does not exist. Nothing above substitutes for it.

The nine models

Every module is TLC-exhaustive at its configured constants, run with -deadlock, zero errors. The numbers below are the ones the proof properties document records from its last run — this table is generated from that file, so the site cannot quote a state count the proof README does not.

The suite is ActIntentPermit.tla, AuthorityJournal.tla, BudgetConservation.tla, EpisodeLease.tla, GreenfieldEnablement.tla, MandateChain.tla, MembershipOfferStanding.tla, Pledge.tla and SubordinateReservation.tla.

Module	Distinct states	States generated	Graph depth
`MembershipOfferStanding.tla`	93	189	8
`Pledge.tla`	40	102	15
`EpisodeLease.tla`	513,776	3,063,256	28
`ActIntentPermit.tla`	61	116	10
`MandateChain.tla`	7,988	18,011	11
`BudgetConservation.tla`	600	2,937	12
`AuthorityJournal.tla`	2,902	6,933	17
`GreenfieldEnablement.tla`	65	121	11
`SubordinateReservation.tla`	900	2,281	9

Safety only — no liveness is claimed, anywhere

Every checked property is safety: state invariants plus action invariants, which are also safety. No specification assumes fairness, so none can promise progress. The reason is honest rather than incidental: every model treats daemon state as durable and a crash as stuttering, and a specification whose crashes are stutter steps cannot promise that anything ever happens. "Every queued episode eventually terminates or expires" is not proved, and cannot be until the sweeper and deadline behaviour is modeled with its fairness assumptions written down.

Bounded, not inductive

All nine are TLC-bounded — exhaustive at their constants, which is not the same as proved for arbitrary run length. Two are flagged as candidates for inductive proof because their bounds genuinely bite: budget conservation at an arbitrary ceiling, and the mandate chain at an arbitrary depth. Today the mandate invariants quantify over chains of depth ≤ 3 at three capabilities; deeper chains are future work.

What each model proves

Every model states four things: its projection (what implementation state is abstracted away, and why that is sound), its refinement boundary (what is claimed to refine it, and where the claim stops), its fairness assumptions, and its bounded-state coverage. That is a requirement of the accepted decision record, not a convention.

Module	The properties it holds, and the interesting one
`MembershipOfferStanding.tla`	Standing exists only through admission; admission requires acceptance; silence never accepts; at most one standing survives the admit/refuse/revoke/expiry race; refusal and revocation fence the coupled onboarding offer in the same transaction; one compute use; completion is evidence, not acceptance.
`Pledge.tla`	A finalized pledge has all its seats; at most one successor; superseded exactly when a successor is accepted — never on amendment alone; terminal states are final; resumes are bounded. Finalization determinism is a guard over an explicit seat receipt set, not a promise.
`EpisodeLease.tla`	No stage of the activation pipeline is skippable; every claim mints one fresh fence and one immutable attempt; a superseded worker's completion never lands; ambiguous is never reported complete. Crash alone never enables a re-claim — an explicit authoritative clock proves that the immediate claim → expire → reclaim trace with no time advancing is impossible.
`ActIntentPermit.tla`	Consume at most once, with exactly one immutable receipt; no consumption without the finalized full seat snapshot; denied, expired and canceled are never consumed and never will be; the consumption key binds the one spent decision. Replay and conflicting-key consumption are explicit actions, so the one-shot invariants are checked against live replay traffic.
`MandateChain.tla`	A child never widens its parent; transitively a grandchild never exceeds the root; non-delegable powers never appear in a child; use ordinals cap; revocation never un-sends prior effects; hold, revocation, exhaustion or expiry of any ancestor fences every descendant's new uses. A widening derivation is attempted explicitly and must fail.
`BudgetConservation.tla`	The conservation identity holds per account in every reachable state; a delegated quantity exists exactly once; settlement cannot spend in two places and a host bridge cannot double-charge; released is a monotonic audit counter rather than a bucket. It refines no descriptor — the budget account is a ledger, not a state machine, and it declares that to the parity checker rather than inventing one.
`AuthorityJournal.tla`	No visible mutation without its witnessed entry; visibility is exactly finalization; the local mirror never outruns the external journal; abandonment only after proving no entry; the witness dedups by transaction id. Against a snapshot/restore adversary: a rolled-back database reopens sealed, and a sealed endpoint mints no entry and widens no visibility.
`GreenfieldEnablement.tla`	No overlapping active owners and no overlapping enablement slots; retry returns the identical binding; no activation after rollback and no rollback of an active epoch; the owner arm flips exactly at the compare-and-set. After amendment A9, "no scope has a third owner" is a type fact rather than an invariant over a value nothing can produce.
`SubordinateReservation.tla`	A subordinate reservation may narrow or deny but never parallel-charge; created once and settled once across lost replies and retries; the recovery query surfaces durable truth, because guessing is not a transition; the only release out of `uncertain` is a governance seat with a fresh challenge.

Modeled, but not everything is

The dual-head effect admission and disposition compare-and-set, the endpoint-incarnation restore lineage, standing mandates, and the assembly machines are all listed in the design's closed-machine section and are not modeled. Neither is kovee's attention and placement internals — only their committed outcomes appear. Two of the C2 machines have descriptor and walk coverage but no model at all.

Descriptor parity, as a gate

Byom commits 26 transition descriptors — 167 states and 312 transitions — in a structured format where every row carries its guards, locks, fences, events and crash result, drawn from a frozen column vocabulary.

Two independent gates hold them in place. One proves that each of the 62 mutating operations on the frozen sheet is owned by exactly one descriptor. The other compares every module's machine-readable parity block against the committed descriptors with exact set equality in both directions: 9 modules, 11 descriptors, 103 states and 199 transitions in exact agreement in both directions, with the structured crash and fence columns compared as well, so a modeled row's crash semantics cannot be swapped even for another legal value.

15 of the committed descriptors have no model. Their machines are listed in the design or are kovee-owned executors; they are registry-checked, schema-checked and walk-checked, and they are not TLC-checked. The per-machine table names which is which →

What parity does not catch

The parity block is a transcription of the model's transition relation — a third copy. The checker catches descriptor drift and annotation drift, and its quoted-literal check catches a state renamed only in the model. It cannot see an edited TLA+ action whose annotation and descriptor were left untouched. TLC still checks the edited model's invariants and the walks still exercise the transitions, which shrinks that window without closing it. Closing it means generating the annotation from the descriptor registry — which lands with the conformance oracle that does not exist yet.

Executable state walks

28 walks — the core machine walks plus the governed-work saga walks — are validated through a small interpreter over the committed descriptor JSON. This is the closed-machine rule as an executable oracle, independent of both TLC and the parity checker, and for the unmodeled C2 machines it is the only executable coverage they have.

The conventions are what make them meaningful:

Every walk starts at absent.
An accepted step must be an exact descriptor row.
A rejected step must be an absent row — an unlisted transition is invalid, and the walk pins that absence.
A replay step retries the immediately preceding mutation and must be state-idempotent.
A {"crash": true} marker restarts the daemon between steps; every descriptor-level variable is durable, so the walk resumes unchanged — which is each machine's committed crash outcome.

They cover, among others: one-shot permit consumption under replay, the expired-lease re-claim as a real transition minting a fresh fence rather than a replay, ambiguous-never-completed, terminal-is-final for every modeled terminal, and the witness-unknown query and abandon-after-proof recovery paths.

The mutation suite

A gate that passes because it checks nothing is worse than no gate. So 14 deliberate mutations are applied to descriptors, models, annotations and schemas, and every one of them must be caught:

a dropped descriptor row, an invented unmodeled row, a renamed state;
a lost structured column, a de-versioned format tag, a dropped parity annotation;
a state literal renamed only in the model;
semantic erasure of a structured column — a crash result swapped for another in-vocabulary value must fail the column transcription, and arbitrary prose must fail the frozen vocabulary;
a widened update meta, and emptied guards;
three weakened TLC guards that must produce counterexamples: a pledge finalizing without its seat set, a re-claim of a live lease head, and an expiry without the clock having passed the deadline.

Separate widening mutations against the MCP tool document run inside the conformance runner on every single invocation.

Vectors and rederivers

462 vectors cover the envelope, the operations, the policy algebra, the governed-work records and sagas, the machine walks and the MCP tool-call bindings, against 234 compiled schemas. Both policy evaluators — one Python, one Node, sharing no code — must agree on every policy case, and a seeded deterministic differential runs them against each other beyond the fixed corpus.

Separately, the family encoding profile's 111 cases across 83 files are re-derived by two more independent programs. That corpus and its rederivers →

The runner also has a live mode: it spawns a real daemon and replays the request vectors against it over the real sockets. That checks the daemon against the wire and against hand-written expectations — not against the models.

What none of this covers

Not covered	Why, and what does cover it
Cryptographic soundness	Signatures, digests and witnesses are modeled as perfect. The models say nothing about the primitives.
Byte-level envelope acceptance	Out of model scope; covered by the family vectors and the runner's acceptance cases instead.
The counterparty's internals	Kovee's attention and placement logic is not modeled — only its committed outcomes appear as inputs.
Timing and side channels	Not modeled at all.
Whether the model matches the design	That remains human review. Conformance can only guarantee that code cannot silently diverge from a transcribed relation — and here, as stated above, even that binding does not exist yet.

Running it yourself

Everything above runs locally, on demand. The commands below are the ones the repository actually runs.

the individual gates from the repository root

python3 conformance/run.py            # schemas, vectors, registry, walks, MCP
python3 proof/check-descriptors.py    # descriptors ↔ models, both directions
python3 proof/negative-checks.py      # the mutation suite (TLC needs java)
python3 family-vectors/xcheck.py      # the profile corpus, re-derived
node    family-vectors/tscheck/check.mjs
make -C proof                         # TLC over every model

everything, in order ./run-checks.sh

./run-checks.sh

That run ends at exit 2, deliberately

Every suite is green and the last stage — the governed-loop gate — reports a skip for its two real-harness cells and refuses to score a skip as a pass. So the script stops before printing its success line. Exit 0 requires the real harnesses; exit 1 is a genuine failure. What that gate does and does not exercise →