There will invariably be some need for a kind of testing. Though we very rarely utilize traditional unit tests. Property-based tests are our common testing entry point.
"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.
"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.