For me, working on contracts on Ethereum, I have found formal methods to be invaluable (we use a tool by Certora [0] based on CVC4 solver). The trade-off shifts

For me, working on contracts on Ethereum, I have found formal methods to be invaluable (we use a tool by Certora [0] based on CVC4 solver). The trade-off shifts once you enter the world of immutable code, and the time we've spent designing, reviewing and now formally testing has been invaluable to shipping our product with confidence. We tend to think of our formal specifications like the ultimate unit test (instead of testing a few cases, test every possible case). Also, the prover has found subtle bugs which have really put a smile on my face. An example spec might look like this: description "Admin (and only admin) can set new admin" { // e0, e1 can hold any possible environment and are ordered sequentially env e0; env e1; // free variable for possible values of new admin address nextAdmin; havoc nextAdmin; // call to set the new admin invoke setAdmin(e0, nextAdmin); // assert one of two conditionals must hold for all cases: // 1. We were the admin and the next admin is what we sent to `setAdmin()` // or 2. We were not the admin, and the next admin is whatever is was before our call to `setAdmin()`. static_assert ( e0.sender == invoke admin(e0) && invoke admin(e1) == nextAdmin ) || ( e0.sender != invoke admin(e0) && invoke admin(e1) == invoke admin(e0) ); } It's a few lines of code to verify a simple function, but it's incredibly powerful for us to know that our code works in all cases. [0] http://www.certora.com/ http://www.certora.com/