We have proof automation now
Formal verification of software, long seen as too costly and specialized, is being reshaped by large language models that can now generate and automate many proofs inside systems like Lean. Commenters argue this could make high-assurance code and even verified assembly practical for more domains, especially security-critical ones, but emphasize that writing good specifications and abstractions remains the hard part and that formal methods can still prove the “wrong” behavior correct if the spec is flawed. There is active debate over how well dependent types and total functions scale in real-world maintenance and whether LLM-driven verification will meaningfully change mainstream software engineering practices or remain focused on critical edge cases.
LLMs + Proof Automation
- Many see LLMs + theorem provers (Lean, HOL-style systems, etc.) as a step-change: they can now discharge large parts of proofs that used to take days or weeks.
- Proof irrelevance plus automation may make rich dependent-type systems more practical, reducing “proof engineering” effort, though good problem decomposition and abstractions are still critical.
- Some describe successful experiments where LLMs recreated multi-day formal proofs in minutes, suggesting previously “insane” verification projects (kernels, major theorems) become plausible solo efforts.
Specifications as the Bottleneck
- Several argue the hardest part is not proving correctness but defining it: real-world software often lacks precise behavior for edge cases (network failures, backups, serializers, etc.).
- Writing formal specs can exceed the length and complexity of the code; bugs in specs directly translate into “verified” but wrong systems.
- Partial specs (e.g., round-tripping, compress/decompress as inverses, “never executes arbitrary code”) are still seen as very valuable.
Dependent Types, Maintenance, and Language Design
- One camp claims dependent types and total functions do not scale for large systems: adding a new property can require threading new invariants through many types and proofs.
- Counterpoint: this is analogous to maintaining correctness in any large system; good structuring (separating concerns, using opaque types, small trusted cores) mitigates the pain.
- Future languages that integrate verification into the type system are viewed as promising, but many expect most programs will only verify critical parts, not whole systems.
Security, Crypto, and Verified Assembly
- Blockchains and crypto are highlighted as prime candidates: strong adversaries, history of formal methods, and interest in verified assembly and compilers.
- As exploit-finding becomes cheaper (including via AI), some argue formal verification becomes economically more attractive; others think organizations will stop at “good enough” automated bug-finding.
LLM Behavior, Alignment, and Limits
- LLMs often avoid heavy proof work unless strongly prompted, prefer superficial solutions, and may ignore powerful libraries unless coerced.
- They can also implement a feature incorrectly and then generate tests/specs that “prove” the wrong behavior, so human review of specs remains essential.
- Enthusiasts see formal methods + LLMs as transformative; skeptics warn this mainly shifts difficulty to higher-level specification and won’t replace testing or human judgment.