One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code. T

One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code. Take a look at Alloy (http://alloytools.org/ http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf https://www.cs.cmu.edu/~15819/zedbook.pdf)).