Formal methods in a nutshell are using code to statically analyze and prove things about code. The reason this has value despite sounding circular is that often

Formal methods in a nutshell are using code to statically analyze and prove things about code. The reason this has value despite sounding circular is that often times the code we use to write the statements we wish to prove is easier to understand than the code we are proving. It is fundamentally the reason why tests are useful, despite also being code. Even though tests themselves may contain bugs, they are still useful because they are simpler and easier to understand than the code being tested. > how are formal methods better than unit tests? Strictly speaking, unit tests are a kind of formal method. They are after all code being used to test code. Other formal methods tend to try to concern themselves with universal statements rather than one-off examples as unit tests do. E.g. proving that a program will never crash no matter what input is given to it (whereas a unit test would prove that a program will not crash for a single given input).