Large Language Models have become remarkably adept at writing code. Systems like GitHub Copilot can generate syntactically correct and often functional snippets of code from a simple natural language prompt. But there's a world of difference between code that looks right and code that is right. How can we be sure that the code an AI generates is free of subtle bugs, edge cases, and security vulnerabilities?

Standard software testing can find bugs, but it can't prove their absence. For the most critical systems—in aerospace, cryptography, and medical devices—we need a higher standard of assurance. This is the realm of Formal Verification (FV), a discipline at the intersection of computer science and mathematical logic dedicated to proving that a piece of software is correct.

Historically, formal verification has been a niche, incredibly difficult, and time-consuming process reserved for a small priesthood of experts. Now, in an unlikely turn of events, the probabilistic, pattern-matching capabilities of LLMs are being brought to bear on the deterministic, logical world of proofs. Can these two fundamentally different paradigms of reasoning actually work together?

• What is Formal Verification? A World of Proofs, Not Tests
• The Unlikely Marriage: LLMs as a Co-pilot for Proofs
  • 1. Generating Formal Specifications
  • 2. Suggesting Proof Tactics
  • 3. Automating Tedious Proof Steps
• The Future: Can an LLM Ever Be the Prover?
• Conclusion: Amplifying Human Reason
  • Further Reading

What is Formal Verification? A World of Proofs, Not Tests

Before we can understand the role of AI, we have to appreciate what formal verification is. Unlike software testing, which validates behavior for a finite set of inputs, formal verification aims to prove that a program adheres to its specification for all possible inputs.

The process generally involves:

1. Formal Specification: A precise, mathematical description of what the program is supposed to do. This might include pre-conditions (requires), post-conditions (ensures), and invariants.
2. Proof Construction: Using a specialized language and an interactive proof assistant (like Coq, Isabelle, Lean, or Dafny), an engineer writes a mathematical proof that the code's implementation satisfies the specification.

This is not like writing a regular program. It's an exacting process of applying logical rules, theorems, and lemmas to construct a machine-checkable proof. It requires the mindset of both an expert programmer and a mathematician. The reward for this effort is an extraordinary level of confidence in the code's correctness, but the cost is immense, which is why it has traditionally been confined to the highest-stakes applications.

The Unlikely Marriage: LLMs as a Co-pilot for Proofs

In their current form, LLMs are not logical reasoners. They are probabilistic pattern matchers. They cannot, on their own, "do" formal verification. A proof that is 99.9% correct is 100% wrong, and the probabilistic nature of LLMs is fundamentally at odds with the need for deterministic guarantees.

However, this doesn't mean they aren't useful. Instead of acting as autonomous provers, LLMs are emerging as incredibly powerful co-pilots for the human experts, dramatically lowering the friction and tedium of the formal verification process.

Here’s how they help:

1. Generating Formal Specifications

Often, the hardest part of formal verification is writing the spec itself. An LLM can take a developer's high-level intent, expressed in natural language, and translate it into a first draft of a formal specification. For example, a developer could write a comment: // This function should take a sorted list of integers and return the median. And an LLM could generate the Dafny specification:

method Median(arr: array<int>) returns (median: int)
  requires arr.Length > 0
  requires forall i, j :: 0 <= i < j < arr.Length ==> arr[i] <= arr[j] // Pre-condition: array is sorted
  ensures exists i :: 0 <= i < arr.Length && arr[i] == median // Post-condition: median is in the array
  // ... more complex post-conditions for correctness

2. Suggesting Proof Tactics

In an interactive proof assistant, the developer often needs to decide which "tactic" or "lemma" to apply to advance the proof state. This can feel like navigating a vast, abstract maze. An LLM, fine-tuned on millions of lines of existing proofs from repositories like Coq's standard library or Lean's Mathlib, can suggest high-probability next steps, acting like a super-powered autocomplete for mathematical reasoning.

3. Automating Tedious Proof Steps

Many proofs involve long, repetitive, and uninteresting steps. LLMs can be tasked with "finishing the job" by automating these boilerplate sections, allowing the human expert to focus their mental energy on the novel and challenging parts of the argument.

The Future: Can an LLM Ever Be the Prover?

While the co-pilot paradigm is powerful, the ultimate question is whether an AI could ever achieve full autonomy in this domain. Could an "AlphaProof" moment be on the horizon?

This would require a shift beyond current architectures, likely towards neuro-symbolic systems that combine the intuitive pattern-matching of neural networks with the rigorous, step-by-step logic of symbolic reasoning engines. A neural component might suggest a creative path forward, while a symbolic component would verify that the step is logically sound.

The fundamental challenge remains the reliability gap. A probabilistic system can never, by its nature, provide the 100% certainty that a proof requires. Any solution would need a final, deterministic verifier to check the LLM's work. The LLM could generate a complete proof attempt, but a separate, traditional, non-AI checker would still have the final say on its validity.

Conclusion: Amplifying Human Reason

LLMs are not about to replace formal verification experts. Instead, they are set to become their single most powerful tool. By translating intent into formal specifications, automating tedious work, and suggesting creative paths forward, AI is poised to drastically lower the barrier to entry for formal methods and amplify the capabilities of human experts.

The unlikely marriage of probabilistic pattern matching and deterministic logic won't lead to machines proving things on their own just yet. But it may be the key to helping us build the next generation of provably safe and reliable software systems, bringing a new level of trust to our increasingly code-dependent world.

Further Reading

1. Lean Programming Language and Proof Assistant
2. Dafny: A language and program verifier for functional correctness
3. Large Language Models for Mathematical Reasoning

Enjoyed this post? Subscribe to the Newsletter for more deep dives into ML infrastructure, interpretibility, and applied AI engineering or check out other posts at Deeper Thoughts