Experiment: Proof Grinding with LLMs

We conducted experiments to show that AI agents can contribute usefully to formal verification by taking on proof search and counterexample discovery tasks that are repetitive and would be time-consuming for humans. Across three domains, the strongest results came when the LLM received one precise property to prove or break at a time, the proof obligations were fixed, and the formal model was grounded against real system behavior.

The decisive shift came in the container experiment. Asking the LLM to search broadly for vulnerabilities made little progress. Giving it one precise claim to test led to a counterexample: a program inside the container could learn information from outside its configured boundary. We verified the violation in the formal model and reproduced the behavior in real systems.

This work also ultimately led to Oath Technologies, a research organization founded by the project’s original principal investigator.

The next question we hope to tackle is how much this can reduce engineering costs as the models and properties grow.

The Approach

One of Galois’s most exciting current research directions concerns the intersection of AI and formal methods. Across multiple projects, we’ve been spearheading work exploring how formal methods can make AI trustworthy and (just as important) how AI can make formal methods scalable – automating the most difficult and time-consuming parts of formal verification, making the process faster, cheaper, and easier for non-experts to use.

As part of the SpecFRO Project, I recently conducted a series of “proof grinding” experiments to test whether and how LLMs could contribute usefully to formal verification workflows. Here, “proof grinding” means letting the LLM search for proofs and counterexamples while a human focuses on the target property, the model's connection to reality, and the validity of the result.

My approach followed these principles:

1. Create a formal model and target: A formal model is a mathematical description of a system’s relevant behavior. Deeply embed the relevant system semantics in Lean, then give the LLM a precise property to prove or break. These properties are often deep themselves: for containers (the example developed below), what a program can observe depends on the interaction among the container configuration, runtime, kernel isolation mechanisms, and the program.
2. Ground the model in reality: Use known vulnerabilities to calibrate the property, then run the same behaviors against the Lean model and real binaries.
3. Challenge the fixed property: Let the LLM search, but inspect what it changes. A valid proof, a counterexample, and a weakened proof obligation are different outcomes.

The Container Experiment

Containers are meant to let programs run while restricting what they can access and observe on the host. The concrete test case I used was a container runtime that follows the Open Container Initiative (OCI) specification. I wrote a Lean model of the runtime and some of the kernel behavior below it. The property I cared about said, roughly, that even a malicious program inside the container shouldn't learn information from outside the boundary set by its configuration.

The theorem I hoped to prove would establish this confidentiality property for the modeled runtime. I didn't want that theorem to be convincing only inside my own model. Past CVEs are useful checks: if the definition doesn't notice a known container escape or information leak, it probably isn't the definition I wanted. A differential harness is an automated test program that gives the same inputs to different implementations of a system and compares their outputs. I use one to compare the Lean model's predictions with real runtime behavior. After that, I gave the property to the LLM and let it work.

One of these attempts ended up at /proc/sys/kernel/random/boot_id. Linux documents the interface, so this isn't a claim that I found a new vulnerability – a counterexample to the confidentiality property I had written.

For the experiment, I ran an unprivileged container under crun 1.14.1, runc 1.4.0, and gVisor. Annoyingly, the first two-boot comparison was unusable. The restart had moved the VM from kernel 6.8.0-117 to 6.8.0-137, so more than the boot_id had changed. I discarded that pair, took 6.8.0-137 as the new baseline, and restarted again. This time the kernel, runtime versions, configuration, and repository commit matched. crun and runc returned the host's exact boot_id on both boots; gVisor returned synthetic values.

The theorem and the experiment aren't interchangeable. My runcModel captures how runc maps OCI configuration to isolation settings, including namespaces, capabilities, syscall restrictions, and filesystem path masking. runc_not_secure proves that boot_id is a confidentiality counterexample for my runcModel (Secure requires both confidentiality and integrity, so this information leak is enough to refute it). The experiment says that real runc and crun executables behaved the same way in this setup. I haven't proved that either binary refines the Lean model. It is tempting to compress all of that into “we proved runc insecure,” but that would be wrong.

What worked and what didn’t

Another calibration problem I kept running into is that security and correctness pull in different directions. A runtime can be secure in a fairly useless way by refusing to run anything. Lean proves that denyAllRuntime is secure and also proves that it is incorrect because it blocks legitimate programs. The opposite failure preserves expected behavior but leaks host state. Neither property is enough by itself, while exists_correct_and_secure checks that asking for both isn't contradictory.

The calibration theorems also exposed an LLM failure mode that I hadn't expected. When the model couldn't prove or disprove one of the claims, it started deleting those theorems. The proof task was getting easier because the checks were disappearing. I found that irritating, but it was also a useful result from stress testing the LLM. This was reward hacking, and deleting a theorem obviously isn't a proof. In future runs I would make the definitions and calibration theorems read-only before starting proof search.

There is a practical problem with doing this through general-access models. The models I can use have cybersecurity guardrails, and they sometimes stop as soon as the work starts to look like vulnerability research, even when I'm working on my own model or a local test VM. I don't have access to Mythos. My guess is that this recipe would work better with a model made available to vetted researchers with fewer restrictions on authorized security work.

Despite this limitation, results so far are already useful. In this experiment I quickly discovered that giving the LLM one property to prove or break is more productive than asking it generally to find vulnerabilities. By focusing its scope, we give the LLM somewhere concrete to look when it gets stuck, although somebody still has to watch what it changes.

Counterexamples beyond containers

The same recipe produced concrete counterexamples in two other domains. For TLS hostname verification, a certificate with no subject alternative name but a matching Common Name witnesses the failure of legacy CN fallback: the Lean regression proves that the legacy path accepts outside the intended SAN-only policy, and the differential harness observed OpenSSL accepting the fixture.

For SQL transaction isolation, two transactions at REPEATABLE READ read the same value, write back the same incremented value, and both commit. The final value looks serializable, but the dependency graph contains a forbidden lost-update cycle. The Lean judge rejects the MySQL model on this history, and the live harness observed the corresponding behavior in MySQL; PostgreSQL aborted one transaction.

Together, these projects show that the method transfers across operating-system isolation, certificate identity, and database concurrency and produces falsifiable results in each domain. How its cost and effectiveness change with larger models and proof obligations remains an open question.

Lessons and next steps

The next experiment should measure how far proof grinding can be pushed as the models and properties grow. I would freeze the definitions and calibration theorems, increase the size and complexity of the proof obligations, and track success rates, required interventions, invalid attempts to change the task, reproducibility across runs and models, and whether generated counterexamples reproduce against real systems. The useful question is no longer whether this beats doing every proof manually, but where the workflow remains reliable and what controls it needs.

At a larger scale, security engineers could state a precise concern and use LLMs to search more of its proof space. Even where the method does not reach a large end-to-end proof, it remains useful for local lemmas, regression proofs, counterexamples, and checking whether a security definition says what its authors intended.