Isn't the problem with formal methods that it isn't clear whether or not most of the useful code we use are actually formally verifiable?

The article mentions NP-complete, but is it actually a solvable problem in general?

> For extremely restricted cases, like propositional logic or HM type-checking, it’s “only” NP-complete.

No, lots of problems can be expressed in a way that can be verified. But complete verification of an existing implementation is essentially impossible.

That doesn't mean that formal techniques are not useful, far from it. For example, AWS uses a formally specified model to verify if an implementation is correct by looking at the telemetry. See e.g.

https://p-org.github.io/P/advanced/pobserve/pobserve/

This isn't something you could meaningfully do with standard testing techniques, and it very compositional, you can do it piece by piece.