"Model conformance" issues can go both directions. The model can diverge from the implementation. The designer's intent can also be incorrectly expressed in the model.
Some forms of testing can be useful in describing the problem domain and expectations in a more approachable/transparent way, and those tests can be used as part of an ensemble of methods to attempt to ensure the model represents the designer's intent, and that the implementation conforms to the model.
It's also extremely unlikely that even if you're able to verify your software, that every other part of the stack/system will have the same assurances, and in those cases some forms of testing can also be useful for building trust in components that you have no proof for.
Disclaimer: this set of problems is what my company works on for life-critical systems.
The emergence of technologies like this and Rust's borrow checker have me dreaming of a future where the writing tests is increasingly unnecessary, as your language requires that you specify your invariants etc up front. That combined with something like QuickCheck may make manually writing test cases a thing of the past.