TL;DR for operators
The strongest result in this case study is not that an AI system wrote working Prolog. Across 33 targeted exercises, Claude generated 508 runtime tests alongside 257 lemmas and roughly 11,800 lines of proof, with the authors manually inspecting the generated files and an independent theorem prover checking the proofs.
That creates a useful separation for high-assurance AI coding: let the model search for implementations, tests, specifications, and proof candidates, but let a deterministic verifier decide which formal claims are accepted. The harder problem remains upstream. Functional-correctness properties frequently required human hints or even a full natural-language formulation before the model could formalize and prove them.
For engineering teams, this suggests that verification infrastructure can constrain what an agent is permitted to claim about its code. It does not remove the need for experts to decide which claims matter.
Passing tests is only one kind of evidence
A coding agent can produce a program that runs and passes every test it was given. The remaining question is what that evidence actually establishes. Tests demonstrate behavior on selected executions; they do not automatically establish termination, uniqueness, output structure, or a functional relationship for every input covered by a formal model.
Mesnard, Marianne, Payet, and Vanhoof examine what happens when those additional claims must themselves survive machine checking.1 Their case study covers 33 of the 88 P-99 Prolog exercises available in their source set. Claude generated 58 logic procedures, 112 Prolog clauses, 150 lines of Prolog code, 508 runtime tests, and 257 lemmas.
The workflow adds an independent acceptance mechanism after generation. The model proposes code, logical properties, and derivations. A theorem prover—LPTP—accepts only proofs that satisfy its formal rules. Invalid or incomplete derivations can be rejected, revised, and resubmitted.
This is the paper’s central methodological contribution. It moves reliability from “the model says its reasoning is valid” toward “a separate formal system certifies a precisely stated property.”
The difficult step was deciding what correctness meant
The aggregate artifact counts could make the workflow appear more autonomous than it was.
According to the paper, generating code and runtime tests was comparatively easy. Formal verification took longer: individual exercises ranged from roughly 15 minutes for P01 to several hours for P35. More consequentially, the authors report that functional-correctness properties often required substantial human guidance.
P01 illustrates the difference between a routine property and a meaningful specification. For my_last/2, the proof set covered termination, types, groundness, membership, existence, and uniqueness. It also established the more informative relationship
together with the converse direction. In plain language, the generated predicate returns exactly the element that can appear as the singleton suffix of the list.
P31 makes the human role clearer. Claude ultimately proved soundness and completeness properties for is_prime/1, but the authors first requested those properties and supplied the intended formalization in natural language.
P35 pushes further. The generated proof set established that prime_factors/2 returns factors whose product is the input, that the list is ordered, that every member is prime, that a factorization exists for positive naturals, and that the result is unique. Those are substantive correctness claims rather than additional test cases.
Yet the proof checker certifies only the properties presented to it. It cannot determine that the chosen properties exhaust everything a user, regulator, or downstream system needs from the program.
That is the critical governance boundary.
Formal verification changes the acceptance process, not specification ownership
The study separates several assurance layers that AI coding products often combine under a broad label such as “validated”:
| Evidence layer | What it establishes | Remaining boundary |
|---|---|---|
| Runtime tests | Selected executions behave as expected | Untested executions remain outside the evidence |
| Routine formal properties | Claims such as types, termination, groundness, existence, or uniqueness hold under the formal model | These properties may still omit the program’s intended function |
| Functional properties | The implementation satisfies a stated behavioral relationship | Someone must choose and formulate the right relationship |
| Machine-checked proof | The submitted derivation satisfies the prover’s rules | Certification applies to the stated property and formal assumptions |
For a high-assurance coding team, Cognaptus infers a practical division of labor from this structure.
Models can be given broad latitude to generate implementations, tests, auxiliary lemmas, and candidate proofs. Deterministic verification tools can then control whether specific claims enter the accepted build or audit record. Experts remain responsible for defining the functional obligations whose failure would actually matter to the system’s users.
The affected decision is therefore not simply whether to allow AI-generated code. It is how much autonomy to permit at each stage: candidate generation, specification, proof construction, and final acceptance.
The evidence supports aggressive automation more strongly for the first and third stages than for the second.
MCP turns the checker into an iterative tool for agents
The paper’s later MCP experiment is best read as an architectural extension rather than a general model benchmark.
The Model Context Protocol interface exposes LPTP grammar, tactics, and proof checking as callable tools. Instead of relying primarily on static prover instructions, an assistant can submit a derivation, receive feedback, revise the attempt, and continue until the result is either formally certified or retains explicit gaps.
On the P14-P24 subset, Gemini 3.1 Pro generated a more diverse collection of properties, while Claude Code using Sonnet 4.6 was the assistant that completed valid proofs for the reported subset. The paper reports certification of the property batches in roughly 40 minutes to one hour of interaction.
The comparison is too small to support a general Claude-versus-Gemini ranking. Its more durable contribution is the interaction pattern: multiple generative assistants can potentially sit in front of the same deterministic verification service.
That reduces dependence on one model’s self-assessment. The verifier defines the acceptance rule.
The production-scale question remains open
The study provides relatively strong within-case evidence because the reported proofs were machine checked and every generated file was manually reviewed. Its generalization evidence is much weaker.
Only 33 of the 88 available P-99 exercises were included in the main experiment. The task family is narrow, the programming language is Prolog under a constrained formal setting, and human intervention was integral to both artifact review and the formulation of difficult correctness properties. The paper itself identifies scalability as unresolved.
There is also no evidence here that an organization can replace established verification or abstract-interpretation systems with LLM-generated properties. The authors explicitly note that existing analysis systems can compute more precise properties.
For production use, the defensible extrapolation is architectural rather than performance-based: generated artifacts can be subjected to independent formal acceptance, and the resulting proofs can be retained alongside code and tests for review.
Whether the same workflow remains economical across larger codebases, richer languages, interacting services, or continuously changing requirements is unanswered.
Verification is strongest when generation does not control acceptance
This case study narrows the role that formal verification can realistically play in AI coding.
A theorem prover can prevent an invalid derivation from being accepted simply because the model presents it confidently. The MCP extension makes that checker accessible inside an iterative coding-agent workflow. Both are concrete mechanisms for placing a non-generative acceptance layer behind a generative system.
But neither mechanism decides what the software is supposed to guarantee.
For high-assurance development, that suggests a three-part architecture: agents generate candidates, deterministic systems certify specified properties, and domain experts determine which properties carry operational consequence. The paper demonstrates that this division can work on a bounded Prolog problem set. The unresolved engineering problem is whether it can scale without making specification and review the new bottleneck.
Cognaptus: Automate the Present, Incubate the Future.
-
Fred Mesnard and Thierry Marianne and Étienne Payet and Wim Vanhoof (2026). Case study: solving P-99 with LPTP and an LLM. arXiv:2607.21196. https://arxiv.org/abs/2607.21196 ↩︎