SOTA on VeriSoftBench and VERINA: Interactive Lean4 Unlocks Frontier LLMs for Vericoding

Research

Can AI-Generated Code Be Trusted?

AI is rapidly changing how software is written. Given a natural-language description, frontier models can now generate substantial programs, debug them, and iteratively improve their own code.

But there is a fundamental problem: how do we know the generated code is actually correct? Today, the primary answer is testing. Testing is enormously useful, but it can only tell us that a program worked on the cases we tested. It cannot, in general, guarantee that the program will behave correctly for every case covered by its requirements.

Formal verification offers another approach. Instead of describing what software should do only in natural language, we express requirements precisely enough that a mathematical system can check them. Lean4 is one such mathematical system. It is both a programming environment and an extremely strict mathematical referee: the AI can propose code and proofs, but Lean determines whether they are valid.

The basic idea we explore involves AI generating an implementation and a proof that it satisfies the specification, and a formal verification system independently checking that proof. Generating software this way is called vericoding. In the benchmark setting we study here, a formal specification is provided as the source of truth. The task is to generate an implementation together with a machine-checkable proof that the implementation conforms to that specification.

Instead of building sophisticated Agent harnesses for such vericoding tasks, we asked the following question to first understand the limits of the combination of LLMs and tools: How Far Can a Frontier LLM Get by appropriately invoking Lean as a tool?

Related Work

Recent work in automated theorem proving and verified code generation has explored specialized prover models such as Goedel Prover [5,6], Seed Prover [10,11], and DeepSeek Prover [2,4]; agentic systems such as HILBERT [7], Inductive-Deductive Synthesis [8], and LEAP [9]; and proprietary systems including Aristotle [3] and Aleph Prover [1].

These approaches have produced impressive results. But frontier LLMs have also improved rapidly in software engineering, mathematical reasoning, and long-horizon problem solving. That raises an important methodological question:

How much performance comes from increasingly sophisticated prover architectures, and how much capability can be unlocked by giving a frontier model effective access to the formal environment itself?

Many formal-proving setups constrain how models interact with Lean4. They may not expose the same interactive features that expert Lean users rely on to inspect definitions, query types, search for applicable lemmas, experiment with intermediate constructions, and understand why a proof failed. It is like evaluating a programmer without giving them an IDE, compiler, debugger, or the ability to experiment. We wanted to remove that constraint.

Tiny Prover

Tiny Prover combines an iterative agent loop with direct, interactive access to Lean4. Rather than generating an entire solution and submitting it only at the end, the model can try an approach, inspect Lean's response to the approach including where it fails, revise its solution, and continue until Lean successfully verifies it.

With the above approach, using gpt-5.4 and opus-4.6 at their highest reasoning settings, Tiny Prover achieves impressive results as follows.

Vericoding results — pass rates by system

System	VERINA	VeriSoftBench — Aristotle Subset
VERINA [12]	20.1% (pass@64)	—
VeriSoftBench [13]	—	65% (pass@8)
Aristotle [3]	96.8%	69%
Inductive-Deductive Synthesis [8]	93.12%	—
Aleph Prover [1]	100%	94%
Tiny Prover (Emergence AI)	100% (pass@1)	98% (pass@1), 100% (pass@2)

VERINA [12] is a high-quality, modular benchmark for verifiable code generation in Lean4, including code gen + spec gen + proof gen, evaluated separately or composed. The benchmark comprises 189 manually curated tasks divided into 2 subsets: Basic (108 problems) and Advanced (81 problems). We evaluate Tiny Prover on the vericoding setting (code gen + proof gen, spec given as source of truth).

VeriSoftBench [13] is a repository-scale formal-verification benchmark for Lean4. Unlike competition mathematics and Mathlib-centric benchmarks, software verification lives in definition-rich codebases. Success anti-correlates with the size of the transitive dependency closure. We evaluate proof generation using the Aristotle subset (100 proofs), a smaller and compilable subset.

During the solving process, we observe that the LLM makes use of various language features:

• Inspection/query commands (#-commands): #check, #eval, #print, #find, etc.
• Search / suggestion tactics: exact?, apply?, rw?, etc.
• Temporary theorem: example.

and more, which are usually not allowed or used in whole-proof generation approaches.

The results show that given the right tools, even a simple iterative approach (like in Tiny Prover) can outperform more complex harnesses.

Some Implications

Future benchmarks will need to move closer to real software engineering: larger repositories, deeper dependencies, longer-horizon changes, implementation and proof generation together, performance constraints, and more complex specifications.

There is also a second boundary to confront. In these benchmarks, the formal specification is provided and treated as the source of truth. In real systems, proving that code conforms to a specification does not prove that the specification correctly captures human intent. As implementation becomes more verifiable, part of the reliability problem moves upstream toward specification fidelity.

But we believe the larger lesson extends beyond Lean and verified code. Much of today's AI stack asks probabilistic models both to generate answers and to judge whether those answers are correct. Formal systems offer another architecture. The neural model can do what it does extraordinarily well: understand intent, reason through complex problems, generate candidate solutions, explore alternatives, and recover from failure. Wherever important requirements can be expressed precisely, an external system can independently determine whether those requirements have been satisfied.

This creates a powerful division of labor:

The model explores. The verifier constrains.

At Emergence, we believe this pattern points toward a broader architecture for autonomous AI. As AI systems receive greater decision-making authority, making the underlying models more capable will not be sufficient. Autonomous systems also need mechanisms that independently enforce the requirements, constraints, and authority within which they are allowed to operate. Not everything in the real world can be formally verified. But wherever important properties can be expressed precisely, they should not depend solely on an LLM judging its own work.

This is the larger idea behind Neuroformal AI: combining the flexibility and reasoning power of neural models with external systems capable of independently checking the parts of their work that must be correct.

---

References

1. Logical Intelligence, "Aleph Prover." Available: logicalintelligence.com/aleph-prover
2. Z. Z. Ren et al., "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition," arXiv:2504.21801, 2025. arxiv.org/abs/2504.21801
3. T. Achim et al., "Aristotle: IMO-level Automated Theorem Proving," arXiv:2510.01346, 2025. arxiv.org/abs/2510.01346
4. H. Xin et al., "DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data," arXiv:2405.14333, 2024. arxiv.org/abs/2405.14333
5. Y. Lin et al., "Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction," International Conference on Learning Representations (ICLR), 2026. proceedings.iclr.cc
6. Y. Lin et al., "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving," Conference on Language Modeling (COLM), 2025. arXiv:2502.07640. arxiv.org/abs/2502.07640
7. S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye, "Hilbert: Recursively Building Formal Proofs with Informal Reasoning," International Conference on Learning Representations (ICLR), 2026. arXiv:2509.22819. arxiv.org/abs/2509.22819
8. S. Agarwal et al., "Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems," arXiv:2605.23109, 2026. arxiv.org/abs/2605.23109
9. P.-N. Kung et al., "LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks," arXiv:2606.03303, 2026. arxiv.org/abs/2606.03303
10. J. Chen et al., "Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience," arXiv:2512.17260, 2025. arxiv.org/abs/2512.17260
11. L. Chen et al., "Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving," arXiv:2507.23726, 2025. arxiv.org/abs/2507.23726
12. Z. Ye, Z. Yan, J. He, T. Kasriel, K. Yang, and D. Song, "VERINA: Benchmarking Verifiable Code Generation," International Conference on Learning Representations (ICLR), 2026. arXiv:2505.23135. arxiv.org/abs/2505.23135
13. Y. Xin, Q. Chen, G. Durrett, and I. Dillig, "VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean," arXiv:2602.18307, 2026. arxiv.org/abs/2602.18307