Formal verification of RTL has always had two taxes: the commercial tool license (JasperGold, Questa Formal) and the human expert who knows how to write the properties. This paper attacks the second with an LLM and the first by wiring it to Yosys, SymbiYosys, and Z3 -- all open source. The pipeline generates formal properties from a specification, runs bounded model checking, and feeds counterexamples back to the LLM until the design is proved correct by k-induction or the iteration budget runs out.
On an ALU case study it detected and repaired a real functional bug and produced a formal proof. On a six-benchmark suite, one design repaired reliably. The honest finding is in the failure analysis: bounded-cover vacuity, specification ambiguity, temporal-logic bugs, and multi-property pressure are the four failure modes the pipeline cannot yet escape. That taxonomy is the most useful part of the paper. It names exactly where the open-source formal toolchain plus LLM breaks down, which is the prerequisite for anyone trying to fix it.
The commercial formal verification vendors have priced their tools on the assumption that formal proof requires both expensive software and expensive humans. An open-source stack that closes even 20% of industrial RTL bugs with a proof replaces a non-trivial fraction of that value. The counterexample feedback loop is the right scaffold for scaling k-induction success rate. If the next model generation doubles it, the 18-month clock starts now for mid-market formal verification licenses.