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).
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).