3 ms·
Isnt the actual proof checking what your traditional formal verification tool does? I would have thought that 99% of the work of formal verification would be wr
by nicoburns 11mo ago
Isnt the actual proof checking what your traditional formal verification tool does? I would have thought that 99% of the work of formal verification would be writing the spec and verifying that it correctly models the problem you are trying to model.
- newAccount2025 11mo agoThe specification task is indeed a lot of work. Driving the tool to complete the proof is often also a lot of work. There are many fully automatic proof tools. Even the simplest like SAT solvers run into very hard computational complexity limits. Many “interactive” provers are more expressive and allow a human to help guide the tool to the proof. That takes intuition, engineering, etc.