Realistically, how much more does AI for coding have to get out of leaning and training more for formal verification (with eg Lean, Rocq etc and their interop with mainstream langs)
If AI hasn’t really pursued this strongly, then maybe a good amount, right?
I can imagine a scenario where you no longer review the code but a simulation of all the behaviours of the system, perhaps before any code has been written, and then you can trust the output will have accordingly …?
What practical limits of formal verification are there for this?
And for the anti AI folks, I’m anti AI too and I don’t use it or want to use it at all. I’m thinking about the future here.
I’m more in the software side of things, but have worked with hardware engineers that use formal verification before committing to a design. How I understand the point of formal verification is to answer the question: does this implementation satisfy the given specification?
With that in mind, I’m having trouble squaring away my definition with your passage:
The whole point, I think, of formal verification is to verify a specific, concrete thing. Simulation doesn’t seem to be remotely relevant at all, because it is not the thing itself. C’est nest pas une pipe. Likewise, formal verification isn’t about stress testing either, such as hardware shock and vibration testing. At bottom, formal is about reducing the thing to its most basic assumptions, and checking those.
If those assumptions turn out to violate the specification, then that answers the question posed earlier. If however the formal process proves that a specific signal within an FPGA will never take longer than 47 ns and another signal always takes longer than 68 ns, then it’s provable that those two signals will not cause a race condition when they come together. And this too answers the question.
Given that formal verification is rooted in mathematical proofs, I don’t see how LLMs can help there. In terms if making formal easier to use regarding inputs and outputs, LLMs are still a poor fit. To trust an LLM to write or even audit the specification that will be inputted to formal verification, that’s adding a very weak link at the very start of a very robust process, essentially negating all the guarantees of formal verification.
As for the output side, I’m not seeing how a yes/no answer from formal could somehow benefit from the mis-confident elaborations of an LLM. Perhaps in the case of a failure result, an LLM can hone in on the exact hardware or software component that the spec violation is occurring. But my understanding is that formal verification software already does that, because that’s the obvious thing to identify once an implementation is proven as faulty.
Formal verification definitely has limits, and one of the greatest limiting factors for its use in the software domain is the fact that compatible software (meaning it can target many platforms, OS, phones, etc) is an utter mindfield to prove correctness for. Just look at memory ordering: x86 and ARM, in the desktop and mobile spaces respectively, behave very different, yet an ideal formal verification would tell us if a race condition could ever arise. We don’t have that today, because the test matrix to verify is outside the limits of our computational power, for any nontrivial example.
Adding AI in any current form – and maybe any future form too – will not change this gap in what can be achieved by raw logic and induction. Formal is simply unbothered by LLMs, neither helped nor hindered.