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.
Enjoyed this series?
Subscribe below to get notified when I publish new series like this one.
Subscribe to newsletter ↓