Formal verification has traditionally been constrained by proof-writing cost. Engineers can state what a program should do, but writing machine-checkable proofs in systems such as Lean, Rocq, Isabelle, F*, Dafny, or Verus requires specialized expertise and substantial labor. LLM-assisted proof generation changes the economics by making the model a proof-script author while a deterministic proof checker remains the authority.
The important distinction is trust placement. The model may hallucinate tactics, lemmas, or implementations, but the proof assistant rejects invalid proofs. A generated proof is only accepted if the kernel, type checker, verifier, or SMT-backed tool confirms that the implementation satisfies the specification under the rules of the formal system.
This creates a practical loop for high-assurance software: write or generate a precise specification, ask an LLM to produce code and proof artifacts, run the checker, feed diagnostics back to the model, and iterate until the proof passes or the system escalates to a human. The hard problem moves from reviewing every generated line of code to defining the right specification and maintaining a robust checker-in-the-loop workflow.
A proof can only establish that code satisfies a stated property. If the property omits a security condition, edge case, or business invariant, a passing proof does not imply the system is correct in the way users care about. LLM assistance reduces proof labor, but it does not remove the need for careful specification design.
The checker is the trust boundary. Lean, Rocq, Isabelle, Dafny, Verus, and related tools reject malformed proof terms, missing obligations, type errors, and unsupported assumptions. This makes proof generation a strong fit for LLMs: invalid output is not silently accepted, and checker errors provide structured feedback for repair.
Most non-trivial proofs require iteration. The agent generates a candidate proof, receives compiler or verifier diagnostics, localizes the failing obligation, retrieves relevant lemmas, and tries a narrower repair. Strong systems preserve the original specification and tests while allowing the model to modify only the proof or implementation region under repair.
Use the LLM as a search procedure over implementations, tactics, and lemmas. Use the proof assistant as the acceptance test that decides whether a candidate is valid.
The workflow begins with a machine-checkable contract. In proof-oriented languages this may be a theorem statement, precondition, postcondition, invariant, refinement type, or ghost-state assertion. The LLM can help draft this contract, but production workflows should review it separately before allowing implementation generation.
// Dafny-style sketch: the specification is executable by the verifier.
method Max(a: int, b: int) returns (m: int)
ensures m >= a
ensures m >= b
ensures m == a || m == b
{
if a >= b {
m := a;
} else {
m := b;
}
}The checker turns the candidate into explicit proof obligations. A failure might identify a missing induction hypothesis, an unsatisfied loop invariant, a type mismatch, or a theorem that cannot be applied. The agent should parse these diagnostics into a focused repair prompt instead of asking the model to rewrite the entire artifact.
Proof repair often depends on finding the right library lemma. The agent can retrieve nearby definitions, theorem names, previous successful proofs, and compiler messages, then ask for a minimal patch. This mirrors software debugging but with a stronger oracle: either the proof checks or it does not.
type ProofAttempt struct {
SpecPath string
CandidatePath string
Diagnostics []CheckerDiagnostic
Retrieved []Lemma
}
func repairPrompt(a ProofAttempt) string {
return fmt.Sprintf(
"Repair only the failing proof block. Preserve the theorem statement. Diagnostics: %v Relevant lemmas: %v",
a.Diagnostics,
a.Retrieved,
)
}If a coding agent produces implementation code, a proof-generating agent can also produce evidence that the implementation satisfies a formal contract. This is strongest for algorithms, parsers, serialization logic, arithmetic, protocol state machines, and security-sensitive helpers where precise properties can be stated.
For high-risk refactors, require the agent to preserve an existing theorem suite or add refinement proofs showing that the new implementation matches the old observable behavior. This changes review from “does the diff look right?” to “do the stated invariants still check?”
LLMs can help translate informal requirements, comments, or paper proofs into formal definitions and lemmas. Human review remains essential because autoformalization can lose subtle assumptions, but the model can reduce the mechanical burden of writing boilerplate definitions and first-pass proof scripts.
Do not let the same unchecked loop weaken the contract it is trying to satisfy. Treat specifications as reviewed inputs. If the model proposes a spec change, route that through a separate review path with clear rationale and regression examples.
pipeline:
- draft_spec:
output: spec.dfy
requires_human_review: true
- generate_candidate:
inputs: [spec.dfy, examples.json]
outputs: [impl.dfy]
- verify:
command: dafny verify impl.dfy
- repair:
inputs: [impl.dfy, verifier_diagnostics.txt]
allowed_edits: ["proof blocks", "loop invariants", "helper lemmas"]Fast feedback matters. Run the proof assistant locally or in an isolated worker after every candidate patch. Capture structured diagnostics, timeouts, and changed obligations so the agent can distinguish syntax errors from hard proof failures.
Many verification systems have escape hatches such as unchecked assumptions, admitted theorems, axioms, disabled termination checks, or trusted foreign functions. A production proof-generation harness should lint for these constructs and fail the build unless they are explicitly reviewed.