Prototype Lean 4 protocol verification alongside TLA+

[kyleve]

Posted by an AI agent on kve's behalf.

Summary

• add a self-contained Lean 4.33.0/Lake package for all nine protocol specifications and all 25 former manifest cases
• add typed transition systems, reachability induction, labelled traces, infinite behaviors, stuttering, weak fairness, and exact diagnostic BFS
• kernel-prove current safety invariants and kernel-check negative-control/reachability witness traces; diagnostic search remains evidence only
• retain TLA+/TLC because three weak-fairness liveness theorems and two deadlock-freedom theorem families are not yet proved in Lean
• add the opt-in ./lean-check, a Lean verification skill, ongoing docs, and immutable Lean/Elan attribution

Recommendation

Keep this PR draft and keep both implementations. Do not adopt Lean as the TLA replacement yet.

Lean is compelling for typed models, unbounded inductive safety proofs, small kernel-checked proof terms, source-reviewable strengthening lemmas, and excellent language/editor tooling. TLC remains materially better for this repository's current workflow when the requirement is automatic bounded exploration, deadlock detection, liveness under fairness, and immediate counterexample traces. This prototype reaches complete finite-case and safety parity but not the required unbounded fairness/deadlock parity. Substituting the diagnostic BFS would weaken the semantics and violate the migration criterion.

A follow-up may delete TLA only after kernel-checking EventuallySettled, DeliveredRemovalEventuallyStops, DeliveredRemovalEventuallyRetires, and deadlock freedom for TrackingReconciliation and RemoteDeviceRemoval.

Language and tooling comparison

Area	TLA+/TLC	Lean prototype	Assessment
State/action model	Mathematical state/action relations; unconstrained values guarded by TypeOK; implicit [Next]_vars stuttering	Algebraic state/action/config types; executable Action → State → Option State; explicit behavior stutters	Lean removes many invalid states at construction, but is more implementation-shaped
Safety	TLC exhausts a configured finite graph	Induction over unbounded Reachable; private strengthening lemmas when public invariants are not inductive	Lean is stronger once the theorem is complete
Counterexamples	Automatic shortest-ish state trace from a violated invariant/temporal property	Checked explicit witnesses plus repo BFS action traces	Lean needs deliberately maintained witnesses/search; TLC is more automatic
Liveness/fairness	Temporal formulas and weak fairness checked automatically over the finite graph	Explicit infinite Behavior, Eventually, LeadsTo, and TLA-compatible WeakFair; proof is manual	Current blocker: definitions exist but three required theorems do not
Deadlock	CHECK_DEADLOCK TRUE	BFS diagnoses deadlocks, but no kernel theorem yet	Diagnostic parity only, not proof parity
Trust	TLC/JVM/tool implementation and finite-model mapping	Lean elaborator/kernel plus Std and theorem/model mapping; no native_decide, custom axioms, sorry, or admit	Lean proof evidence has the smaller proof-validation story; both depend on model fidelity
Reviewability	Compact relational specs and configs; counterexamples are easy to inspect	Typed definitions and theorem scripts are familiar code, but inductive strengthenings add proof maintenance	Mixed; Lean is better for local invariants, TLA is better for temporal intent
Editor/build	TLA+ Toolbox and TLC CLI	Lean language server, Lake incremental build, Elan pinning	Lean editor feedback is excellent; cold distribution is much larger
Dependencies	TLC jar plus Java	Lean self-contained toolchain plus Elan; no Veil, Mathlib, or LeanLTL	Prototype dependency graph is intentionally minimal
Maintenance	Bounds/configs and source mapping; temporal automation	Proofs, strengthening lemmas, checked witnesses, search, and source mapping	Lean shifts recurring cost from runs into proof authoring

Lean's reference says successful build means the kernel accepted the theorem; it also explains why decide remains kernel-reduced while native evaluation expands trust. Lake is the standard incremental package/build tool and Elan reads a checked-in version-specific lean-toolchain. TLA+ is intentionally a high-level mathematical specification language, and TLC is its engineering-oriented model checker. Sources: Lean reference, proof validation, Lake, Elan, TLA+ overview, TLC repository/tooling.

Alternatives evaluated

• Veil 2.0 preview is the closest Lean-native TLC-style workflow, but the branch labels itself a pre-release with bugs/rough edges and describes liveness as future work. Its additional Mathlib/SMT/Node stack would also prevent this prototype from evaluating plain Lean.
• LeanLTL is useful semantic prior art for finite/infinite linear time and tactic integration, but the published work is a reasoning framework, not an automatic TLC replacement.
• The Lean/TLA state-machine comparison discussion reinforces the central tradeoff: transition closure is natural to prove inductively, while temporal automation and usable counterexamples require additional machinery.

Parity matrix

Specification	Cases	Lean safety theorem(s)	Broken/reachability witnesses	Diagnostic parity	Liveness/deadlock parity
IngestorQuiesce	2	yes	broken	yes	n/a
IntentServicesHandoff	2	yes	broken	yes	n/a
LaunchLifecycle	2	yes	broken	yes	n/a
LogRouting	2	yes	broken	yes	n/a
PostWriteReconcile	2	yes	broken	yes	n/a
ScopeExclusivity	2	yes	broken	yes	n/a
StorePerformSerialization	2	yes	broken	yes	n/a
TrackingReconciliation	6	yes	broken + stale reachability	all six	blocked: EventuallySettled and deadlock theorem
RemoteDeviceRemoval	5	yes	broken + two reachability controls	all five	blocked: two delivered-removal liveness theorems and deadlock theorem
Total	25	9/9 safety families	9 broken + 3 reachability	25/25	3 liveness + 2 deadlock families missing

Benchmarks

Measured on Apple Silicon macOS 26.5.2 on 2026-08-12. RSS is /usr/bin/time -lp; download/storage figures are artifact/cache sizes, not committed bytes. Typed representation intentionally changes state counts.

Measurement	TLA+/TLC 1.7.4	Lean 4.33.0
Full suite wall time, warm	45.1s baseline run	2.7s
Full suite peak RSS	513,851,392 B (~490 MiB)	387,350,528 B (~369 MiB)
Cold setup + full run	approximately 45s observed baseline including setup activity	55.6s
Download	2.2MB TLC + approximately 336MB Temurin	2.1MB Elan + 556.2MB Lean
Installed cache	338MB	2.7GB
Largest current case	Remote multiple: 678,105 generated / 113,648 distinct, 8s TLC case	Remote multiple: 5,865,993 generated / 610,401 distinct; included in 2.7s suite

The Lean search uses exact equality through Std.HashSet; hashes only index buckets. Its results are diagnostic and are not referenced by any theorem.

Validation

• ./tla-check baseline: all 9 specs / 25 cases passed before prototype work (45.07s, 513,851,392 B peak RSS)
• final ./tla-check TrackingReconciliation RemoteDeviceRemoval: all liveness/deadlock configurations and controls passed
• ./lean-check: all 9 modules built; all 25 diagnostic cases matched expectations
• ./lean-check --list: listed all 9 models
• ./lean-check StorePerformSerialization: selected model passed
• ./lean-check UnknownSpec: exited 1 with the expected unknown-spec error
• cold ./lean-check: 55.64s, 795,459,584 B peak RSS; original caches restored afterward
• warm ./lean-check: 2.68s, 387,350,528 B peak RSS
• bash -n lean-check
• no sorry, admit, new axiom, or native_decide in Lean sources
• ./attribution and ./attribution --check
• ./swiftformat --lint
• ./sync-agents and skill-creator validation
• git diff --check

Swift test suites skipped: this is opt-in formal-model/tooling/documentation work and changes no Swift production behavior.

Limitations

• The Lean models are source-mapped abstractions, not refinements mechanically extracted from Swift.
• Several ports use proof-oriented inductive strengthenings; those are reviewable but add maintenance.
• The two large protocol ports normalize finite sets and queues differently from TLA; compare violated property and event sequence, not graph size/depth.
• Diagnostic BFS currently enumerates the large RemoteDeviceRemoval case aggressively; its speed is good on this machine but its 2M-state cap is a prototype policy.
• No CI change is proposed.
• TLA files, manifests, runner, skill, and attribution deliberately remain because full semantic parity is not green.