3 ms·

So, like writing code and then writing tests for it?

• chimpburger 8y ago
  Not really. Formal verification methods are mathematically rigorous. They can mathematically prove or disprove correctness of programs and catch bugs that would be extremely difficult for a human to find https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification
  • youeseh 8y ago
    "Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior." It sounds a lot like writing your specs as tests that are then satisfied by the implementation code.
    • deleted 8y ago
      [deleted]
    • chimpburger 8y ago
      TLA+ is for building and verifying a formal model of the program (a blueprint), not for verifying the implementation.