Extensive functional testing Vs Formal verification

Found this on James Hamilton's blog (quoting Butler Lampson at SOSP) :
"Problem is that testing is expensive, so there is a trade-off between extensive testing and cost. Essentially you can’t test everything. This is part of the reason why the lowest levels of the system need to be simple enough to formally reason about their behavior."
A similar thought had been running in my mind following repeated discovery of some "corner cases" in a recently released feature. The problem was that, in the absence of QA engineers (yes, can you believe it!), testing by by developers was never going to be sufficient. In response, I had proposed:
1) Listing system invariants.
2) Formally proving that (based on the current implementation of various operations exposed by the interface), these constraints would not be violated. This would have helped us single out systemic issues much earlier and would not have necessitated hand-writing expensive integration for various scenarios. That way, the functional tests could be better utilized to test other scenarios (than verifying if system invariants hold at all times).
On a related note, there must be a way of specifying these invariants formally and have a utility generate test cases against a given API? Have you heard of any?