Formal Verification Gets a Moment in the Sun
A post about hunting a 16-year-old SQLite WAL bug using TLA+ made the front page and the author showed up in the comments. The bug lived in SQLite for over a decade before formal modeling found it. The thread was warm, with multiple commenters expressing genuine love for TLA+ and one wondering about porting it to Lean and building tactics for it.
This sits alongside the Leanstral thread, which is specifically a proof-abundance model built on Lean 4 and is trying to make formal verification cheaper and more accessible. Taken together, these two threads suggest formal methods are having a quiet resurgence, driven partly by the fact that AI code generation is raising the stakes on correctness.
The counterpoint: TLA+ has been having 'a moment' on HN for years, and the gap between enthusiast interest and production adoption remains wide.
So what?
For founders building infrastructure, databases, or distributed systems, the SQLite story is a concrete case that formal verification finds bugs that testing misses, and finds them decades faster. If your correctness guarantees are a selling point, look at what TLA+ or Lean-based tooling can do for your review process.