If for verification, I'll add this trifecta some of us independently arrived at:<p>1. Formal specs drive spec/property-based testing for quick verification.<p>2. If that passes, try to get automated proof with the solver.<p>3. Use formal specs as runtime checks or traces that get checked with the input being from fuzzers or other test generatore. Failures take you right to the property that failed.<p>4. Optionally, leave runtime check in for any specification property that is unproven or lacking resources to prove.<p>Also, static analyzers that quickly catch certain kinds of problems. If available, I'd run them in parallel to the property-based testing <i>before</i> the proof attempt. All this together keeps time/effort minimized with productivity on verified code maximized.
We’ve been using Certora for smart contract code verification. For me, it’s really amazing to see effective code verification can be (on small and important code routines). Over time, I expect code verification to overtake unit testing for core (pure) code modules.