Ask HN: Is formal verification of practical use in real world projects? 5 pointsakkad338 months ago4 commentsSaveHideCopy link On HNComments−wmf8moFormal verification is useful for security-critical software (e.g. the new AWS hypervisor) or low-level distributed systems components (e.g. Paxos/Raft implementations).−akkad33OP8moDo you know what tools they use?−wmf8moTLA+ is a big one.−IntelliAvatar8moFull formal verification is rare, but partial guarantees at execution boundaries are very practical — especially for systems that act autonomously.
Comments
Formal verification is useful for security-critical software (e.g. the new AWS hypervisor) or low-level distributed systems components (e.g. Paxos/Raft implementations).
Do you know what tools they use?
TLA+ is a big one.
Full formal verification is rare, but partial guarantees at execution boundaries are very practical — especially for systems that act autonomously.