Thanks and thanks for the interesting read. I've been looking for real uses of formal verification for a long time. I've played a lot with code contracts in C# and I've played some with languages like Eifel - the advantage of this approach is that it's static and it performs actual proof rather than enforcement.

These forms of formal verification could really help with building robust software and if someone makes them easy enough to use I can definitely see them as useful alongside if not instead of unit tests.