Verifying behavior is great and all if you can actually exhaustively test the behaviors of your system. If you can't, then not knowing what your code is actually doing is going to set you back when things do go belly up.
not exactly valuable as guidance since programming languages are very easy to verify, but the https://ghuntley.com/ralph post is an example of whats possible on the very extreme end of the spectrum