Recent experiment on ~fully autonomous TLAPS proofs for Raft with Opus 4.6.

Preliminary takeaway: can complete non-trivial inductive invariant proofs with close to 100% autonomy (> 40 minute agent runs w/ no human input).

will62794.github.io/formal-methods…

Vol:18 No:12 → Design and Modular Verification of Distributed Transactions in MongoDB vldb.org/pvldb/vol18/p5…

Consensus protocols are hard, and dynamic reconfiguration (replacing failed machines w/ new ones) is even trickier. I wrote about our use of formal methods in MongoDB to design a novel, "logless" reconfiguration protocol quickly and confidently.

mongodb.com/company/blog/t…

The protocol is formally specified and verified in TLA+, and, for fun, you can also take it for a spin in this interactive protocol visualization:

will62794.github.io/spectacle/#!/h…