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.