Re:Formal Verification Creates Hacker-Proof Code (2016)
by lmm on Monday April 27, 2020 @09:08PM
(#23002205)
But you have access to everything at every stage. There's no need to figure out what the data is or how it got that way - the hard part of debugging - because there is no data, no state, no user input. It's more like fixing a compilation error than debugging.
A proof can fail for many reasons, and even in the simplest possible case, where the tool provides you with a counter example it could either be a real bug in the design/program/protocol, but there could also be something wrong with the specification you were given, or in your implementation of the specification, or in some assumptions you've made to simplify the proof, or there's ambiguity in the natural language description, or even some typo somewhere.
You now need to understand the domain and the system well enough to come up with an explanation of the phenomena. This is debugging.