> formal methods are worth it, but they're not a substitute for being careful.
Yes. Exactly this. I hereby dub this Tombert's law. :-)
I'm honored! I always thought Tombert's Law would end up being something about cartoon trivia, so this is much better.
Formal methods are super cool, and formal verification is even cool, but it can be really easy to think it's always perfect. It gives you such amazing guardrails most of the time that it can be easy to stop looking for when there aren't any.
For example, model checking is cool and useful, but sort of by definition it is exhaustive and as a result you end up having to restrict scope in a lot of cases (For example, redefining the INTEGERS set to {-1000...1000} in TLA+). This is almost always perfectly fine and can catch a lot of weird cases, but it's easy to forget that "nearly everything" is not the same thing as "everything".
Obviously I still think formal methods are worth it, but they're not a substitute for being careful.