How this is proven

A green test suite is not an argument. A guarantee is only worth what its tests can falsify, so each one here is broken on purpose and the test written for it must fail.

Testing

postgres.rs, a2a_interop.rs and vault.rs need a Docker daemon or a foreign implementation, and are skipped rather than failed without one — so they stay compiled and exercised by just test on every machine, between the rarer runs that have both.

A format checks itself against its own bytes, not against its own reader

Two of the entries above are checked-in artifacts rather than assertions: tests/golden/records.jsonl (one canonical record per kind, with its chain digest) and tests/golden/export.jsonl (a sealed export). They exist because a test that serialises and then deserialises proves only that the build agrees with itself, and the failure they catch is the one that passes every such test: a serde attribute renamed, a skip_serializing_if added, the canonicalization rule changed — each rehashing every record this project will ever write, each reading in review as a tidy-up.

Both are sealed through the production path, never re-derived. A vector generator that serialises the value equivalently pins the equivalence rather than the format: canonical form sorts object members, so a corpus built with serde_json directly is sensitive to struct declaration order — which the chain does not depend on — and blind to the canonicalization rule, which is the whole of what it does depend on. The bytes come off Record::seal, the one function every backend appends through, so there is no equivalent way to produce them.

Regenerating them is a separate command:

AGENTPLANE_BLESS_GOLDEN=1 cargo test --test trust format::

Deliberately not a --fix, and deliberately not automatic. Until the format freeze a shape change is a hard cut — every journal written by an older build stops being readable — so blessing the corpus is the moment somebody decides that, and it should cost a decision.

The corpus is read by something that is not this crate

Vectors a project generates and then checks are that project agreeing with itself. They catch drift; they cannot catch a shared misunderstanding, because there is only one understanding present.

tools/verify_export.py is the second one. It is written from the published record format and reads none of this crate’s Rust, which is a property a guard enforces rather than a promise — a verifier that consulted src/ would be a paraphrase of the implementation and would agree with it by construction. It runs in the gate, and it does three things:

just verify-golden

• --canon-check re-derives all 33 record vectors from their parsed values — an independent canonicalizer, an independent chain digest. This is the half that produces bytes rather than accepting them, and it is non-circular: the input is what each record means, the output is what the format says it must look like. It also holds both implementations to RFC 8785’s own number vectors, the one part of canonicalization no record reaches.
• The default pass verifies the sealed export: chains, log positions, the Merkle root, the case layer, the frame.
• --self-test damages that export — an edited readable body, a flipped wire byte, a record removed from the middle, a rewritten log leaf, the case layer dropped, the trailer cut off, a framing member from a later writer — and asserts each one is reported. A second reader that answers 0 findings for everything agrees with this crate perfectly and is worth nothing.

What it still does not buy: it is one reader, written by the same project, from a specification that project also wrote. A genuinely independent implementation by somebody else remains the strongest evidence available, and this is the next best thing rather than a substitute for it.

The size a proof starts from is stated, never inferred

Witness::cosign takes old_size from the caller. That looks like ceremony and is not: an RFC 6962 consistency proof is O(log n) hashes, not one per new entry, so nothing about a proof reveals which size it starts from. A 50→100 proof carries seven hashes, and an implementation computing size - proof.len() claims to start at 93 — which every witness refuses.

Only the holder of the log knows. MemoryWitness checks the caller’s claim against what it remembers and reports a mismatch as Stale, exactly as a remote witness’s 409 does, so the in-process model stays a faithful stand-in rather than a friendlier one — including the cosignature timestamp, which is non-zero because the specification forbids the value that would say no clock of record.

A four-entry log with a two-hash proof is the one size where the wrong arithmetic gives the right answer, so the test uses fifty and a hundred.

The fake witness performs the check the specification makes mandatory

A witness MUST verify the checkpoint signature against the public key(s) it trusts for the checkpoint origin, and answer 403 Forbidden when it does not verify. The stub in tests/wire/witness_http.rs does that, deriving the key id and the note framing from the specification’s words rather than by calling this crate’s helpers.

It matters because a stub that skips it accepts a signature made over some other checkpoint — which is a client that submits one signature forever and is refused by every real witness, while passing every test in the file. The test that pins it submits two different checkpoints, since a fixed signature over the first note satisfies a single-checkpoint test.

The specs are mutation-tested

Model checking proves a spec’s invariants hold of the spec. It says nothing about whether those invariants constrain anything, and the difference is not visible by reading.

tla/EffectProtocol.tla models “act” and “record” as separate steps. As one atomic step TLC explores it exhaustively and finds no errors — but the one state the protocol exists to survive, the action landed and the process died before recording it, is unreachable, so ExactlyOnce holds by construction. Green, and worthless.

So tla/verify.sh runs two passes. The first checks the specs. The second checks the check: each spec is re-run against deliberately broken copies of itself, and each mutant must be caught by the specific invariant written for it — or, for a liveness claim, must make TLC report that property violated: a claim that still holds once the fairness it rests on is dropped holds for some other reason than the one stated. Every .tla is checked; there is no list to add a new one to. A selection — the full table, one entry per mutant, is tla/mutations.py (python3 tla/mutations.py --list):

Tripping the top-level Safety conjunction is not accepted — that shows only that something broke, not that the invariant aimed at this bug is the one that caught it. A mutation that no longer matches its spec is a failure too: a mutation that changes nothing tests nothing.

Every crash point, without a fault injector

A crash truncates an append-only journal, which means the journal enumerates its own fault schedules: every prefix of a real journal is a crash that could have happened. tests/engine/simulation.rs runs a workload, then for each prefix builds a fresh store holding exactly that much history, resumes it, and checks the specs’ invariants against the code. For a run of n records that is n crash points, exhaustively — no seed, no injector, nothing to get lucky with. It sweeps a run that succeeds and a run that unwinds.

What it does not do is reorder writes, skew clocks, partition a network, or stall a disk. That needs the runtime on a simulated executor, and is the layer above this one.

The assertion that bites is about failures, not outcomes

The obvious check — no effect performed twice — is nearly vacuous here, and the reason generalises. Exactly-once is enforced at two layers: replay reads a completed effect back from the journal, and beneath it the store keys effect starts by (run, effect_key). Delete the replay path entirely and the world still contains no duplicate, because the re-announcement is rejected one layer down. The sweep goes green over a runtime that has stopped replaying at all.

So the load-bearing assertion is: replay must never reach the constraint. A resume may refuse, but only for a reason the design names — a crash before PlanFrozen, or an undecidable outcome under a recovery mode that forbids guessing. Being saved by the unique index is the backstop catching what replay should have caught, and the test says so by name.

The general rule: a property enforced at more than one layer cannot be tested by observing the outcome, because the outer layer masks every inner failure. The test must assert which layer held.

Every guarantee is broken on purpose, in CI

The specs are mutation-tested; so is the code. tools/verify-mutants.sh walks a checked-in table of mutations — one per load-bearing guarantee — applies each, runs the suite, and requires the test written for that guarantee to fail.

The distinction between “some test failed” and “the named test failed” is the whole point. A mutation caught by an unrelated test is reported weak, because it usually means the guarantee has no test of its own: the one holding it up can be rewritten, or deleted as redundant, without anyone noticing what it was protecting.

Two things are errors rather than skips. An anchor that no longer matches means the code moved and the mutation is silently testing nothing. A mutation that fails to compile broke the file instead of removing the guarantee — it proves nothing either way.

It exists because a guarantee can be implemented, tested, and unfalsifiable: a test whose name claims a property its body cannot exercise passes forever, and only removing the guarantee shows it.

tests/guards/layering.rs checks that every test the table names actually exists — an invented name otherwise costs a full rebuild to discover.

The model and the code are pinned to each other

A verified spec and a passing suite can still be checking different things. The dangerous direction is a spec gaining an invariant the Rust side never implements: the model then verifies a protocol the runtime does not have, and a green TLA+ job reads as assurance about code it says nothing about.

So every_spec_invariant_is_claimed_by_a_test in tests/guards/layering.rs holds an explicit map from each spec invariant to the test that checks the same property of the implementation, and enforces it in both directions — renaming either side fails the build. An invariant added to a Safety conjunction with no counterpart fails it too.

tests/guards/layering.rs deserves a note more generally: it checks properties that no amount of code review reliably catches, because they are about what is absent — a missing lint entry, an accidental serde_json/preserve_order, an I/O import creeping into core, an invariant nobody wired up, a telemetry event nobody emits, a public enum variant nothing constructs, a pair of features nothing exercises together.

A variant, a recovery mode, an error or a record kind declared and never built reads as a capability the system has. #[from] variants are exempt (? builds them), and a variant meant for callers counts only if a test constructs it.

The model↔code guard maps each invariant to one test, so two features each tested on its own can still break each other — a replan whose successor reuses a completed step’s id makes an unwind compensate work that never ran. Adding a feature widens where an invariant applies, so the widening is what gets checked — every pair of the feature axes must be exercised together, or declared independent with the reason.

A guard that reads source must exclude the source that is the guard. A dead-variant check reads its own doc comment naming an example, and an interaction matrix reads its own detection literals as a test exercising every feature. So they strip comments, and the matrix skips layering.rs.