Vero: Can AI Agents Build Formally Verified Software Repositories?

• URL: http://arxiv.org/abs/2608.13522v1
• Date: Thu, 13 Aug 2026 17:41:27 GMT
• Title: Vero: Can AI Agents Build Formally Verified Software Repositories?
• Abstract summary: Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
• Score: 45.09790101960906
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.

Related papers

• SWE-Gate: Passing Functional Tests Is Not Enough for Software Engineering Agents [63.65682461568621]
  We introduce SWE-Gate, a repository-level benchmark for software engineering agents that explicitly evaluates review constraint compliance alongside functional correctness.<n>SWE-Gate derives review constraints from real pull request review comments and synthesizes repository-level repair instances around these constraints.<n>Each instance provides separate functional and constraint tests, together with non-compliant and gold patches, enabling explicit separation between issue resolution capability and review constraint compliance.
  arXiv  Detail & Related papers  (2026-09-03T17:53:34Z)
• Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
  We introduce Protocol-Driven Development (PDD), where the primary software artifact is a machine-enforceable protocol rather than code.<n>PDD defines a governance model for automated software engineering.
  arXiv  Detail & Related papers  (2026-05-13T04:23:14Z)
• RepoZero: Can LLMs Generate a Code Repository from Scratch? [13.87780777614509]
  RepoZero is the first benchmark that enables fully automated, execution-based verification of repository-level generation from scratch.<n>Our results establish RepoZero as a challenging, scalable, and reliable testbed for end-to-end code generation.
  arXiv  Detail & Related papers  (2026-05-08T01:56:02Z)
• BUILD-AND-FIND: An Effort-Aware Protocol for Evaluating Agent-Managed Codebases [0.0]
  We introduce BUILD-AND-FIND, a protocol for evaluating whether downstream agents can recover intended choices from generated repositories.<n>For each task, a builder sees a hidden repository specification and creates a specification-traced multiple-choice question bank.<n>The protocol separates behavioral correctness from artifact-side recovery and reports recovery accuracy, repeatability, implementation coverage, and inspection effort.
  arXiv  Detail & Related papers  (2026-05-07T12:35:27Z)
• Code Broker: A Multi-Agent System for Automated Code Quality Assessment [0.0]
  We present Code Broker, a multi agent system built with Google Agent Development Kit ADK.<n>It analyses Python code from files, local directories, or GitHub repositories and generates actionable quality assessment reports.
  arXiv  Detail & Related papers  (2026-04-25T00:53:59Z)
• RepoMod-Bench: A Benchmark for Code Repository Modernization via Implementation-Agnostic Testing [1.4069797812477614]
  We introduce a benchmarking framework for repository-level code modernization built on an implementation-agnostic evaluation paradigm.<n>RepoMod-Bench is a benchmark of 21 real-world repositories with standardized interfaces, spanning 8 languages.<n>The benchmark contains 1.6M lines of code (LOC) and 11,616 tests, with repository sizes ranging from 14 to 211K LOC.
  arXiv  Detail & Related papers  (2026-02-26T01:25:00Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0 is a benchmark that challenges AI agents to write libraries from scratch.<n>Agents are provided with a specification document outlining the library's API as well as a suite of interactive unit tests.<n> Commit0 also offers an interactive environment where models receive static analysis and execution feedback on the code they generate.
  arXiv  Detail & Related papers  (2024-12-02T18:11:30Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  We present the Code-Development Benchmark (Codev-Bench), a fine-grained, real-world, repository-level, and developer-centric evaluation framework. Codev-Agent is an agent-based system that automates repository crawling, constructs execution environments, extracts dynamic calling chains from existing unit tests, and generates new test samples to avoid data leakage.
  arXiv  Detail & Related papers  (2024-10-02T09:11:10Z)
• RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generation [96.75695811963242]
  RepoCoder is a framework to streamline the repository-level code completion process. It incorporates a similarity-based retriever and a pre-trained code language model. It consistently outperforms the vanilla retrieval-augmented code completion approach.
  arXiv  Detail & Related papers  (2023-03-22T13:54:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.