For people interested in the idea of formal verification, you may want to look at TLA+ (https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2

For people interested in the idea of formal verification, you may want to look at TLA+ (https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B) and PlusCal (https://en.wikipedia.org/wiki/PlusCal https://en.wikipedia.org/wiki/PlusCal), which have been mentioned on HN before. They're a specialty system for writing code (and mathematical proofs) where every possible system behavior for a given range of inputs can be examined for safety (outputs within allowed ranges with no unexpected behavior) and for liveliness (the expected progression from one output to another).