Technical writing
These writeups show the kind of work I do for protocol teams: turning ambiguous distributed-system behavior into executable specifications, model-checking campaigns, and test harnesses.
More technical write-ups are on Protocols Made Fun →
Proving safety of Tendermint consensus with Apalache and AI
Repairing a TLA+ inductive invariant with Apalache and AI assistance, then building machine-checked safety proofs for single-height Tendermint in TLAPS and Lean 4.
AI-assisted conformance testing of ZooKeeper
Extracting a formal specification from a real distributed system and using Apalache + AI-assisted harnesses to explore failures around leader election, TCP disconnects, persistence, and recovery.
Interactive symbolic testing of TFTP
A compact protocol-testing lab showing how symbolic exploration finds behavior that conventional hand-written tests tend to miss.
Proving completeness of an eventually perfect failure detector in Lean 4
Formalizing partial synchrony, fairness, and infinite executions, then proving strong completeness of an eventually perfect failure detector in Lean 4.