Formal model of the Zanii log
ZaniiLog.tla is a TLA+ model of the design in ../SPEC.md: per-agent
receipt chains, revocation, signed tree heads, on-chain anchoring, and an independent
monitor. TLC explores every reachable state of the model within fixed bounds and
checks that the safety properties below hold in all of them.
Tests show the code does the right thing on the cases someone thought to write down. Model checking shows the design does the right thing in every interleaving of concurrent writers, monitors and a dishonest operator, including the ones nobody thought to write down.
Results
| Config | Operator | Must | Result | States explored |
|---|---|---|---|---|
honest.cfg |
honest, concurrent writers and fork attempts | pass | pass | 212,531 |
adversary.cfg |
dishonest: truncates and alters what it serves | pass | pass | 68,712 |
vacuity.cfg |
dishonest | fail | fails as required | 435 |
toctou.cfg |
honest, monitor without pinned proofs | fail | fails as required | 1,236 |
What is checked
| Property | Meaning | Config |
|---|---|---|
NoFork |
An agent's chain never forks: never two receipts naming the same predecessor | honest |
RevocationRespected |
Nothing an agent records is accepted after its delegation is revoked | honest |
AppendOnly |
Every signed tree head extends every earlier one | honest |
AnchorsHold |
Everything ever anchored on chain is still a prefix of the log | honest |
NoFalseAlarm |
An honest log never makes a correct monitor alarm, however writes interleave with its checks | honest |
MonitorNeverRewinds |
Whatever the operator does, the history a monitor accepts never rewinds — a rewrite can make it alarm, never make it accept a different past | honest, adversary |
RewriteAlarms |
Checking a head that does not extend the accepted history always alarms | honest, adversary |
AnchoredRewriteAlarms |
A head that contradicts an anchor at or below its size always alarms, even for a monitor with no prior state | honest, adversary |
NoFork and RevocationRespected are guarded by the server's two ingest checks: the
submitted prev must equal the agent's current head, and the agent must not be
revoked. Removing either guard from the model breaks the corresponding property.
The two configurations that must fail
vacuity.cfg asks whether the adversary can actually rewrite history in this
model. It can — TLC finds a signed head that does not extend an earlier one. That is
what makes adversary.cfg passing meaningful: the monitor properties hold against
real rewrites, not because rewrites were impossible to begin with.
toctou.cfg models a monitor that fetches a signed head, then requests a
consistency proof without pinning it to that head's size. TLC finds this six-step
trace on an honest log:
- a receipt is accepted
- the operator signs a head over it
- a second receipt is accepted — the tree grows
- the monitor fetches the signed head from step 2
- the monitor checks it: the server proves against its current tree, the monitor verifies against the older head's root, the proof fails
- false alarm — on a log that never rewrote anything
This is the race that produced false "history was rewritten" alarms in production,
fixed in @zanii/monitor 0.2.0 by requesting GET /v1/consistency?first=m&second=n
pinned to the fetched head. honest.cfg runs the same model with pinned proofs and
NoFalseAlarm holds in all 212,531 states.
Running it
Needs Java 11 or later and tla2tools.jar from the
TLA+ releases:
python protocol/formal/check.py --jar /path/to/tla2tools.jar
The runner checks each configuration ends the way it must. A configuration that should fail but passes is reported as a failure too, since it would mean the model can no longer express what it exists to rule out. The whole suite runs in about 15 seconds.
What this does not prove
Stated plainly, so it is not over-read:
- It assumes the cryptography. A Merkle root stands for the log view it commits to, and a consistency proof verifies exactly when one view is a prefix of the other. That holds under SHA-256 collision resistance; the model does not prove it. Signatures are assumed unforgeable.
- It checks the design, not the code. The model mirrors the rules the server and monitor implement. A bug in the implementation that the design does not have is invisible here; that is what the test suites and cross-language vectors are for.
- It is bounded. Every state within the bounds is explored, not every state of an unbounded log. The bounds are small on purpose — most protocol bugs need only a few entries and steps to show, as the six-step race above does.
- A monitor protects only what it has seen or what is anchored. An operator can rewrite entries that no monitor has observed and no anchor covers yet. Anchoring frequency bounds that window, which is why the log anchors on a schedule.