Formal verification is not new. It's been around for at least 40 years. The founders of model checking even got Turing award back in 2017. All major chip makers use formal verification to verify their circuit designs. Microsoft published papers more than 10 years ago on how they use model checking to verify Windows kernel. It was a pretty big thing when people formally verified the IEEE cache coherence protocol. Universities have been teaching formal verification and model checking for over 20 years. The list goes on. What TLA+ offers, though, is amazing usability to engineers who had no interesting studying temporal logic in depth or all kinds of mathematical logic in general. Previous generation of engineers who want to use model checking had to deal with atrocities like this: https://matthewbdwyer.github.io/psp/patterns/ctl.html#Univer.... Yeah, I'm not kidding, the simplest spec would take days if not weeks for engineers to master, if they can master them at all.

> but this extra non-debuggable step actually seems like it would be worse. Not really. Some types of bugs are just too hard to be spotted by mere mortal, or too expensive to catch in production. Case in point, do you know there's a subtle bug or at least ambiguity in the description of Paxos Made Simple? I don't know how many hundreds of people have read the paper, but I doubt if more than 100 of them spotted the bug. Similarly, Amazon hired about 20 experts in formal verification to help them catch elusive flaws in specifications. After, if S3 corrupts customer data, the consequence to the S3 team can be devastating, no?