Proofs · Assurance

The rules are not only prose.

Akson's security claims live in three places at once: the design document, TLA+ models a checker explores end to end, and the Rust state machines. Tooling holds all three together — so the code cannot drift silently from what was modeled, and what was modeled is checked against every interleaving of its world.

7 TLA+ models TLC + Apalache 2 proved unbounded 19 harness self-tests independent cross-checker

Three copies, held together

A design that only exists as prose drifts. A model that only exists in a paper never meets the code. Akson keeps all three, and makes divergence loud.

TLC exhaustively explores each model's configured world — crashes at every commit point, endless replays, hostile deliveries — and Apalache removes the run-length bound for two modules. The traceability — which design section, which threat, which invariant, which enforcing function — is a table per model in proof/PROPERTIES.md.

Seven models

Each model is small, adversarial, and aimed at one part of the protocol where a subtle interleaving could break a promise.

Model	The world it checks
`TaskLifecycle`	One requester, one performer, a network that may replay every message forever, a daemon that may crash between any two commit points. The attempt machine is the implemented sandboxed-run transition table from `akson-authority` (the trusted `task fulfill` edge is not yet modeled — see limits).
`ContractChain`	The contract revision chain's compare-and-swap head, transcribed 1:1 from `akson-contract`, under adversarial delivery: replays, competing siblings, skipped revisions, forged predecessors, stale acceptances.
`ReceivePipeline`	The real commit order of receiving a proposal — peek, validate, head write, input persist, idempotency commit — with crashes between any two writes and a sender free to put any body under any message id, forever.
`PairingLedger`	The consume-once bootstrap ledger behind pairing invitations, under adversarial transcripts and nondeterministic expiry and purging.
`BrokerBudget`	Processor calls under one work order: the sub-attempt machine plus the in-transaction budget count, with crashes mapping mid-flight calls to `ambiguous`, never to a retry.
`RollbackAdversary`	An attacker who restores database snapshots to replay consumed one-shot nonces. With rollback detection on, the invariant holds; with the interim custody (detection unavailable), TLC is required to produce the attack trace — the threat model's residual risk as a machine-checked counterexample instead of prose.
`TaskLiveness`	The one honest liveness claim: every issued work order eventually reaches a terminal state or expires — assuming time advances, a crashed daemon eventually restarts, crashes are finite, and the daemon enforces deadlines. The worker gets no fairness: the property holds even if it never claims or hangs forever.

The invariants, in plain language

A selection of what the checkers prove over every reachable interleaving of those worlds — the full list, with the enforcing Rust function for each, is in PROPERTIES.md:

Invariant	Means
`AtMostOnceEffect`	The worker really starts at most once, across every crash-and-replay schedule.
`DurableBeforeEffect`	The durable record advances before the first byte of any effect leaves.
`NoAuthorityWithoutApproval`	Arrival is not execution: no reachable state holds authority that a local approval did not create.
`OneShotWorkOrder`	A work order is claimed at most once, ever — its nonce cannot be reused. ("Ever" assumes the store is not rolled back; interim custody cannot yet detect a rollback — see the attack trace.)
`AmbiguousNeverDone`	An attempt interrupted by a crash surfaces as `ambiguous`, never as success — and nothing ever leaves `ambiguous` automatically.
`OneTaskPerBody`	However many times a proposal is replayed, exactly one task exists for those bytes, and duplicates are answered byte-identically.
`LockIsFinal` · `AtMostOneLock`	Accepting a contract locks exactly one revision digest, and nothing — replay, sibling, forged predecessor — changes it afterwards.
`AtMostOnePeer` · `NoRevival`	A pairing invitation creates at most one peer, ever; a consumed or expired invitation cannot be brought back.
`BudgetBound` · `AtMostOneTransmit`	No interleaving of calls and crashes exceeds the approved operation budget, and an uncertain call is never silently retransmitted.
`OneShotNonceForever`	With rollback detection, a consumed nonce stays consumed across any number of snapshot/restore cycles — proved inductively for arbitrary generation counts.

Model ↔ code, as CI

A model of the code is worthless the day the code changes. So the models are pinned to the implementation by tests that run with the ordinary workspace suite.

proof/conformance is a workspace member. For every (state, event) pair, it asserts that the implemented pure transition functions equal the TLA+ transition relations: akson-authority::next against TaskLifecycle (49 pairs), akson-broker::next against BrokerBudget (36 pairs), and akson-contract's apply_revision/accept_head against ContractChain's guards, exercised with real parsed contracts. A change to either side that forgets the other fails plain cargo test --workspace — it cannot land quietly.

What this does and does not catch

The oracle is a hand-transcribed relation table, not a parse of the .tla files. It catches code drift — a Rust change that contradicts the transcribed relation fails the suite — but editing a .tla action and nothing else would not, because the transcription is a third copy. Generating the oracle from the specs is tracked follow-up work; the current guarantee is that the code cannot silently diverge from the transcribed relation.

Beyond bounded runs

TLC checks exhaustively, but within configured state-space sizes. For two modules, Apalache discharges the full inductive argument — base case, consecution, and implication — removing the run-length bound entirely:

PairingLedger: all six pairing invariants hold after any number of steps.
RollbackAdversary: OneShotNonceForever holds for arbitrary generation counts and any number of snapshot/restore cycles.

The other five models remain exhaustively checked at their configured sizes; extending induction to BrokerBudget and ContractChain is the named next step in PROPERTIES.md.

Testing the tests

A model checker that never finds anything might be checking nothing. The harness proves its own teeth.

make negative runs 19 self-tests: ten mutated models that each break one protocol rule on purpose — TLC must produce the counterexample trace; four probes whose deliberately false claims must be refuted; a differential, a temporal-fairness dependency, two induction vacuity guards, and an induction-collapse mutant showing the inductive proof genuinely rests on rollback detection:

make negative — excerpt

ok    probe: settlement is reachable
ok    retry-after-crash: Invariant OneShotWorkOrder is violated
ok    no-dedup:          Invariant NoDuplicateTask  is violated
ok    ind-no-detection:  consecution collapses without the counter
…

The same discipline runs the other way: the RollbackAdversary model with detection disabled must fail, producing the concrete attack trace for the threat model's open custody risk. When the real keystore backend lands, flipping that switch to "must hold" is the definition of done.

An independent second opinion

Model checking can't tell you your SHA-256 is over the wrong bytes. For everything byte-precise, a second implementation has to agree.

Golden vectors cover JCS canonical bytes, JWK thumbprints, DSSE pre-authentication encoding and signatures, agent-card JWS, delivery commitments, pairing transcripts, I-JSON acceptance, manifests, and outcomes.

xcheck/ re-derives every vector with Python libraries that share no code with the workspace. This has already paid for itself: the jcs/utf16-key-sorting vector caught serde_jcs sorting object keys by Unicode code point where RFC 8785 requires UTF-16 code units — which is why the workspace uses json-canon instead (ADR-0001).

Below the byte level, fuzz targets (contract, ijson, sarif) and hostile-input suites hammer the parsers the models treat as atomic.

What is not proved

A proof page that hides its edges would be advertising. These are the edges.

Cryptographic soundness. Ed25519, HMAC, and DSSE are modeled as perfect primitives. Akson uses reviewed implementations; it does not re-prove them.
Sandbox escape. Kernel-level isolation is enforced and probed, not formally verified — that is the kernel's problem statement, not a TLA+ one.
Timing and side channels. Out of scope in the threat model, and out of scope here.
One liveness gap, on record. The liveness model assumes the daemon drives every claimed attempt to a terminal state at its deadline. The code enforces a wall-clock ceiling once task run starts, but an attempt that is approved and then never run has no deadline sweeper yet — so termination is proved of the model, and holds of the code only for attempts that actually run. PROPERTIES.md carries this note verbatim until the sweeper lands.
One unmodeled edge, on record. task fulfill — the trusted, operator-only path — completes a claimed attempt without entering running. The modeled, conformance-tested machine only reaches success through running; the fulfil edge is not yet in the model, and reconciling the two is tracked work.
Interim custody. Until the real keystore backend, rollback detection is unavailable — and rather than pretend otherwise, the harness requires the attack trace to exist (see above).

Run it yourself

The conformance suite needs nothing beyond the Rust toolchain; the checkers fetch themselves on first use (Java 11+ required). The harness's own documentation is proof/README.md:

any host

cargo test --workspace        # includes proof/conformance — model ↔ code

cd proof
make             # exhaustively check every spec (TLC)
make inductive   # Apalache: same invariants, any run length
make negative    # the harness proves its own teeth
make full        # all of the above

A passing check ends the only way it should:

tlc — TaskLifecycle

Model checking completed. No error has been found.
1602 states generated, 697 distinct states found, 0 states left on queue.