Fero puts programming agents before a full-repository test, not a single-function test

A programming agent can write code that works in a small example, but the question becomes much harder when the task is distributed across an entire repository and across modules that depend on one another. The new “Fero” paper does not introduce a new agent, but builds a benchmark to test this kind of ability: can the agent choose to execute the code and at the same time produce a proof that the machine can verify against the required specifications?

The paper starts from a clear gap. The use of AI agents in programming is expanding, but the code they generate does not itself guarantee correctness. Generating verified code, however, combines execution with a proof read by an automated verification tool. Researchers consider this path a stronger route toward AI-generated software that can be trusted.

The benchmark does not stop at the solution

Existing benchmarks either focus on single functions, or test proof generation after the implementation has already been provided. Fero moves to the repository level, evaluating the generation of both implementation and proof together in multi-module code. This choice tests whether the agent can make coherent decisions between the program’s structure and the proof of its specifications, rather than solving an isolated part of the task.

The benchmark consists of 43 multi-module cases drawn from real repositories that include Python, Dafny, Verus and Coq. The cases span cryptographic protocols and distributed systems. Each case is a Lean 4 multi-module repository containing predefined APIs, formally selected specifications, and reference implementations. This enables two evaluation modes: proof only, or code and proof together.

Even the reference needs verification

Fero does not treat the specifications and reference implementations as infallible. A verification mechanism has been added that allows agents to prove that a given specification is unimplementable, or that the reference code is incorrect. The purpose is to expose hidden errors in code or specifications and to correct them while constructing the benchmark. This detail changes the meaning of the test: success is not merely producing an acceptable output, but handling a formal contract that may itself be subject to review.

The result delineates the limit of current capability

The researchers evaluated advanced programming agents with access to Lean tools. The strongest agent solved only 27 of the 43 cases completely, and did not close any specification in the hardest repositories. This result does not mean that agents are not useful for programming, but it clarifies the gap between generating code suggestions and building a coherent repository that can be automatically verified at scale.

The paper’s value is not in a quick promise of software safety, but in making the gap measurable. It provides a testing environment and a toolkit for preparing and evaluating cases, and then shows that verification at the repository level remains harder than current capabilities can overcome. For teams considering introducing programming agents into sensitive work, this is a practical signal: evaluation should not stop at running the code, but should ask what can be proven about it.