The term "formal methods" covers a wide range of stuff, though. Basically we're just talking about mathematically rigorous approaches to code. The high-water-m

The term "formal methods" covers a wide range of stuff, though. Basically we're just talking about mathematically rigorous approaches to code. The high-water-mark, which is stuff like formal proof of correctness or proof of worst-case runtime, gets a lot of attention; but there are plenty of valuable approaches that are less expensive. You can do, for example, formal proof of the absence of runtime exceptions (e.g. no bounds check violations), which doesn't require a formal specification and tends to result in a lot of theorems that are easy to prove automatically. Or you can do data and information flow analysis, which will let you verify that you don't depend on uninitialized values of variables or make sure that your expectations about how different inputs to a program should affect outputs ("hey, why doesn't the weapon release discrete depend on the weight-on-wheels sensor?")