Building a Formal Verification Tool from Scratch
A deep dive into building a TLA-based formal verification tool from scratch. Learn systems programming, virtual machines, parsers, compilers, and formal method by building a real tool.
- 1
Building a Formal Verification Tool from Scratch: Part 1 (Die Hard Edition)
What if you could explore every possible timeline of your distributed system to find the bugs you haven't imagined yet? I'm building a TLA model checker from scratch to understand how formal verification works
- 2
Building a Formal Verification Tool from Scratch: Part 2 (The Virtual Machine)
Hardcoded solvers don't scale. We need an engine that operates purely on logic to verify any system. We build a custom Virtual Machine in Odin, tackling instruction sets (bytecode), tagged unions, and the subtle traps of memory identity.
- 3
Building a Formal Verification Tool from Scratch: Part 3 (Rethinking the Foundation)
We take a step back to rethink the foundation. Replacing dynamic arrays with fixed-size registers, upgrading our hash function, and learning why simple data structures make things easy.
Stay Updated
Subscribe below to get notified when new posts in this series are published.
Subscribe to newsletter ↓