Formal Verification Complete: TLA+ model checking — 136K states, 8 safety invariants, zero violations

[arcadamarket]

Phase 1 of formal verification for the RAG Runtime Kernel state machine is complete.

What was verified

We wrote a 555-line TLA+ specification encoding the exact transition table, WAL (write-ahead log) semantics, proposal lifecycle, and crash/recovery behavior from the Python runtime (rag_kernel/state_machine.py and rag_kernel/persistence.py).

The TLC model checker exhaustively explored 136,193 states (84,261 distinct) in 6 seconds.

Results: 8 safety invariants — all passed

Invariant	What it checks
TypeInvariant	Every variable holds a value of its declared type
TransitionSafety	Current state is always reachable from BOOTING via legal edges
SingleWriter	At most one proposal staged at a time
WALConsistency	WAL is append-only, monotonically sequenced, never lags state
TerminalSafety	Once in CLOSING, state never changes
NoDeadlock	Every non-terminal state has at least one enabled action
CrashRecoveryConsistency	crashed=TRUE implies state=RECOVERY
WALPrecedesStateChange	WAL entry for new state written before stateSeq advances

Bug found and fixed

TLC discovered a genuine BOOTING↔RECOVERY livelock — RecoveryComplete could nondeterministically choose BOOTING over READY indefinitely. This was not caught by 337 unit tests.

Fix: Strengthened fairness from WF to SF on RecoveryComplete(READY), ensuring recovery always eventually reaches READY. This matches the Python implementation’s deterministic behavior.

Liveness properties (Phase 2)

Three temporal properties are defined but deferred:

• EventualProgress — after any crash, system eventually reaches READY
• EventualTermination — CLOSING is maintained forever once entered
• ProposalEventuallyResolved — staged proposals are never left pending

These need a model with WAL truncation/compaction to avoid false positives from the finite bound.

Files

All formal verification artifacts are in formal/:

• RAGKernel.tla — TLA+ specification (555 lines)
• RAGKernel.cfg — TLC model configuration
• TLC_RESULTS.md — detailed results

What’s next

Phase 2 will add WAL compaction to the model and verify liveness properties at full depth. Phase 3 will auto-generate transition guard code from the formal model. Phase 4 will embed those guards into the Python runtime.

See the full roadmap for details.