The hardest part of formal verification was never running the prover. It was writing the specification in the first place. Over the years I have watched capable Solidity teams buy into formal methods, spin up a prover, and then stall for weeks because nobody could translate "the vault must stay solvent" into a machine-checkable property. A recent line of research flips that bottleneck: instead of a human hand-writing every specification, a language model drafts the formal properties, and a second model reasons about whether those properties hold. This is where I think LLM-driven formal verification actually earns its keep.
Why property writing is the real bottleneck
Symbolic provers are powerful, but they are only as good as the properties you feed them. An empty spec file proves nothing. In my experience, the specification language itself is the barrier: expressing an invariant such as "total shares are always backed by at least the deposited assets" requires you to know the codebase, the prover's semantics, and the quirks of the spec dialect at the same time. Most engineers never clear all three hurdles simultaneously.
That gap is exactly what LLM-generated properties target. If a model can propose plausible, compilable specifications for a contract it has never seen, then formal verification stops being a specialist ritual and starts looking like a tool a normal audit team can pick up in an afternoon.
How PropertyGPT generates formal properties
The most cited result here comes from PropertyGPT, published at NDSS 2025. Its core idea is retrieval-augmented property generation. The authors collected 623 human-written properties from 23 Certora projects and embedded them into a vector database. When you point the system at new code, it retrieves the most similar reference properties and uses them as in-context examples so the LLM (GPT-4 in the paper) can transfer that human expertise onto your contract. It is, in effect, RAG applied to formal specs instead of chat answers.
What makes this more than a prompt trick is the feedback machinery around generation. Raw LLM output rarely compiles cleanly, so PropertyGPT uses compilation and static-analysis errors as an external oracle, feeding them back so the model iteratively revises the property until it is syntactically valid. It then ranks candidates across multiple similarity dimensions with a weighted algorithm to pick the top-K, and hands those to a dedicated prover for actual formal verification. Generation, revision, ranking, proving — a pipeline, not a one-shot call.
The headline numbers are what convinced me to take it seriously. Against a human-written ground truth, PropertyGPT reached roughly 80% recall (covering 80% of the equivalent properties experts wrote by hand) with about 64% precision. On real vulnerabilities it detected 9 of 13 CVEs and 17 of 24 attack incidents — 26 of 37 total — and on live bounty programs it surfaced 12 confirmed zero-day findings worth $8,256 in rewards. For a system that writes its own specs, catching two-thirds of known incidents is a genuinely strong signal.
Retrieval in practice: from reference spec to new property
Concretely, when you want an LLM to generate formal properties for Solidity, the flow looks like this. Suppose your contract exposes a deposit and withdraw on an ERC-4626-style vault. The retrieval step pulls a reference invariant from a similar audited vault — something a human once wrote in a verification language:
// retrieved reference (human-authored)
invariant totalAssetsBacksShares()
totalAssets() >= convertToAssets(totalSupply());
The model then adapts that pattern to your code's actual function and variable names, producing a candidate such as:
// LLM-generated candidate for the target contract
invariant sharesNeverExceedBacking()
_totalShares <= assetToken.balanceOf(address(this)) + investedAssets;
If that candidate fails to compile — wrong getter name, missing ghost variable — the compiler error is returned to the model, which rewrites it. Only survivors get ranked and proven. The important shift is that a human reviews and prioritizes generated properties rather than authoring each one from a blank file. That is a very different, much lower-friction job.
The verification oracle: an LLM that judges validity
Generation is half the story. A separate 2025 study, "LLMs as verification oracles for Solidity," asks a sharper question: can a reasoning model itself decide whether a given property is valid or violated, and explain why? The authors ran the first systematic evaluation of a frontier reasoning model (GPT-5) on a large benchmark of verification tasks, comparing its verdicts against established formal tools.
The result surprised me: an overall F1 of about 92% at predicting property (in)validity. More interesting than the raw score is the coverage. Symbolic tools like SolCMC or a Certora-style prover can only reason about properties expressible in their spec language. The LLM oracle produced meaningful verdicts even on properties those tools cannot encode at all — and it surfaced mismatches between the developer's intent and the formal specification, which is often where real bugs hide.
I want to be precise about what this is and is not. A verification oracle here means a model that predicts and justifies validity — it has no soundness guarantee. A symbolic prover that returns "verified" gives you a mathematical certificate; a reasoning LLM gives you a well-argued opinion that is right ~92% of the time. Those are different products. The oracle is a triage and coverage layer, not a replacement for a proof.
A practical workflow I would actually run
If I were folding these ideas into an audit today, I would treat the LLM as the spec author and first-pass reviewer, and keep a real prover as the source of truth:
- Index your reference properties. Gather previously written specs (yours or public audited projects) into a vector store so retrieval has good examples to transfer from.
- Generate candidates per contract. Let the model draft properties for each critical function and state variable, with compiler feedback wired in so only compilable specs survive.
- Rank and shortlist. Keep the top-K by similarity and relevance instead of drowning reviewers in dozens of near-duplicates.
- Run the oracle for triage. Use a reasoning LLM to predict which properties likely hold and which are probably violated, plus its explanation — this tells you where to look first.
- Prove the survivors. Hand the shortlist to an actual symbolic prover. A "violated" verdict with a counterexample is your bug; a "verified" is your guarantee.
- Read the disagreements. Where the oracle and the prover disagree, or where the model flags an intent/spec mismatch, is where I spend my human hours.
Limitations and where I stay skeptical
I will not oversell this. The 80% recall and 64% precision from PropertyGPT mean one in five expert properties is still missed, and roughly a third of generated candidates are noise you must filter. The oracle's 92% F1 is impressive but carries no soundness guarantee — you cannot ship a model's "looks valid" as if it were a proof. Both systems inherit LLM failure modes: hallucinated getters, plausible-but-wrong invariants, and sensitivity to how the contract is presented. Retrieval quality caps everything; if your reference corpus lacks anything like the target pattern, generation degrades. I treat these as force multipliers for a human who already understands formal methods, not a way to skip that understanding.
Frequently Asked Questions
Does PropertyGPT replace writing Certora Verification Language specs by hand?
Not entirely. It automates the drafting by transferring human-written CVL-style properties onto new code, but a person still reviews, prioritizes, and proves the shortlist. It changes authoring from writing to editing.
What does "verification oracle" mean here?
It is an LLM that predicts whether a formal property is valid or violated and explains its reasoning. It is a probabilistic judgment (~92% F1), not a sound mathematical proof, so it complements a symbolic prover rather than replacing it.
How reliable is an 80% recall in practice?
It means the system reproduced about 80% of the properties experts wrote by hand, with ~64% precision. Strong for automation, but you should assume some real properties are missed and some generated ones are noise — human review is non-negotiable.
Can the LLM oracle check properties a symbolic prover cannot?
Yes, and that is its most useful trait. It produced verdicts on properties not expressible in spec languages used by tools like SolCMC, widening coverage — though without the certainty a prover provides.
Conclusion
What I find compelling about this research is the division of labor. Retrieval-augmented generation attacks the authoring bottleneck by turning a corpus of human-written properties into drafts for new code, and a reasoning-model oracle attacks the interpretation bottleneck by triaging which properties likely hold. Neither gives you soundness on its own — that still belongs to the symbolic prover. But together they lower the entry barrier that kept formal verification locked behind specialists. My honest take: use the LLM to write and triage properties, use a prover to trust them, and spend your scarce human attention on the places where the two disagree.
