Hacker News new | past | comments | ask | show | jobs | submit login

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



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


TLA+ is for building and verifying a formal model of the program (a blueprint), not for verifying the implementation.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: