LLMs are making formal software verification feasible at a much larger scale

LLMs, Formal Verification, and Capability Limits

• Several comments connect Anthropic’s results to the “convex hull” idea: LLMs interpolate within human mathematical practice but may struggle to invent fundamentally new abstractions.
• Some argue LLMs are strong at grinding through large, known-style proofs but will hit complexity walls without better abstraction and reasoning strategies.
• Others counter that reinforcement learning on harder tasks might yield emergent better proof strategies, so the limit is not clearly fixed.

Proof Style, Abstraction, and Complexity

• Agent-generated proofs are described as extremely verbose, expanding every low-level execution detail.
• This mirrors how LLMs write code and tests: brittle, concrete, repetitive, weak modularization.
• Multiple people note that scaling verification will require human-like proof engineering: modular abstractions, reusable lemmas, and better reasoning principles.
• There is optimism that training on good proof structure could improve general coding quality, especially in strongly-typed functional and Rust-like ecosystems.

What’s Actually Verified? Specs, Models, and Limits

• Strong emphasis that “formally verified” always means “with respect to a formal spec/model,” which may not match real intent or real hardware.
• Concern that LLMs can generate vacuous or mis-specified theorems that still pass the checker, giving false confidence.
• Some highlight classic limits (halting problem, Rice’s theorem), while others stress these don’t prevent proving useful properties for specific, non-arbitrary programs.
• Distinction drawn between verification (code matches spec), validation (spec matches real-world needs), and the difficulty of the latter.

Workflows, Tools, and Levels of Abstraction

• Several practitioners report success using LLMs with Lean/Rocq, ESBMC, Alloy, Verus, etc., especially for equivalence proofs (e.g., C→Rust rewrites, optimizations vs reference implementations).
• Verifying compiled binaries or LLVM IR is seen as powerful but “brutal,” requiring large, machine-generated proof terms; this is exactly where LLM scale shines.
• Others argue equivalence-to-a-golden-reference is more tractable than full specs and well-suited to legacy systems (e.g., COBOL, Postgres C).

Declarative Futures vs Imperative Reality

• One camp predicts a shift toward deterministic declarative languages with rich type/effect systems and built-in verifiability, making formal proofs the default.
• Skeptics doubt a sufficiently flexible, performant declarative language can avoid becoming effectively imperative or re-creating the “sufficiently smart compiler” problem.
• Discussion touches on DSLs, embedded declarative fragments (SQL, LINQ, Inform7), and distributed systems semantics.

Testing, Fuzzing, Security, and Adoption

• Many see the main practical win today as: prove fuzz-test properties hold for all inputs (no crashes, round-trips, algebraic laws), yielding stronger guarantees than fuzzing alone.
• Debate over whether this is “real” formal verification or just supercharged testing, but most agree it’s still a substantial step up for security and robustness.
• Some are excited about lowering the barrier to tools like Alloy, TLA+, and formal methods in safety-critical or high-assurance domains; others predict limited adoption outside “paranoid” niches.

Socioeconomic and Workflow Concerns

• Several developers describe LLMs as simultaneously empowering (faster experimentation, more verification) and demoralizing (loss of craft, fear for career stability).
• There is worry that industry will spend LLM “verification dividends” on more velocity and sloppier systems rather than genuinely higher assurance.
• A recurring theme: LLMs amplify existing tendencies—sloppy teams generate more slop; careful teams can push into verification that was previously too expensive.