A couple recent examples of formal methods in the real world: 1. Elasticsearch in 2019 using formal methods to think through their new cluster coordination algorithm between versions 6 and 7. https://lnkd.in/eMKAwV4E (Ctrl-f for "formal" 2. AWS this year released Cedar, a formally verified (with Dafny) authorization language. https://lnkd.in/epBjPaP3 3. PingCAP using TLA+ to formally verify their Raft implementation and distributed transactions in TiDB. https://lnkd.in/e_yD_6Kd You can also see a much larger (and slightly older) list on https://lnkd.in/enVN2Kz5. And follow folks like Jack Vanlightly, Hillel Wayne, Murat Demirbas, and David Pearce who often write about formal methods.
I've always wondered - is there much use of building formally verified software on top of non-formally verified systems (like the OS the software runs on)? To me, the absolute layman here, it feels like we're building proofs on top of potentially/probably flawed axioms. If we can verify Raft is a solid algorithm but it's built on non-verified networking devices do we end up putting a wrong amount of trust into the system? Edit: Is there a set of formally-verified software out there all the way down the stack? Formally verified application on top of a formally verified language on top of a formally verified OS etc?
More background on #1 https://conf.tlapl.us/2019/yannickwelsch/
Formal Methods | Software Engineering | Software History
1yI should probably write more formal methods stuff on LinkedIn, huh