Vero: 인공지능 에이전트가 형식적으로 검증된 소프트웨어 저장소를 구축할 수 있는가?

Vero: Can AI Agents Build Formally Verified Software Repositories?

인공지능 에이전트는 점점 더 많은 분야에서 프로그래밍에 활용되고 있지만, 생성된 코드의 정확성을 보장하지는 않습니다. 검증된 코드 생성이란 에이전트가 구현과 함께 해당 구현의 명세에 대한 머신 기반 검증 증명을 동시에 생성하는 방식으로, 신뢰할 수 있는 인공지능 생성 소프트웨어 개발을 위한 강력한 방법입니다. 이 분야의 기존 벤치마크는 개별 함수에 집중하거나, 제공된 구현에 대한 검증 증명만 평가하는 데 그치는 경우가 많습니다. 아직까지 에이전트가 실제 다중 모듈 코드베이스에서 일관성 있는 구현 및 검증 선택을 수행할 수 있는지 여부는 미지수입니다. 이러한 격차를 해소하기 위해, 저장소 수준에서의 공동 구현 및 검증 합성 성능을 평가하는 최초의 벤치마크인 Vero를 소개합니다. Vero는 Python, Dafny, Verus, Coq 등 다양한 프로그래밍 언어로 작성된 43개의 다중 모듈 인스턴스를 포함하며, 암호화 프로토콜부터 분산 시스템에 이르기까지 다양한 도메인을 포괄합니다. 각 인스턴스는 미리 정의된 API 인터페이스, 수동으로 작성된 형식 명세 및 참조 구현을 갖춘 다중 모듈 Lean 4 저장소로 구성되어 있으며, 검증 증명만 평가하는 모드와 코드 및 검증 증명을 모두 평가하는 모드를 지원합니다. Vero는 벤치마크의 신뢰성을 향상시키기 위해 에이전트가 제공된 명세의 불성립 또는 참조 코드의 오류를 형식적으로 증명할 수 있는 감사 메커니즘을 포함하고 있으며, 이를 통해 명세 및 코드 작성 과정에서 발생하는 잠재적인 오류를 발견하고 수정할 수 있습니다. 우리는 Lean 툴체인 접근 권한을 가진 최첨단 코딩 에이전트 구성을 사용하여 Vero를 평가했습니다. 가장 강력한 에이전트는 43개의 인스턴스 중 27개만을 완전히 해결했으며, 가장 어려운 저장소에 대해서는 어떠한 명세도 해결하지 못했습니다. Vero는 현재의 에이전트가 아직 부족함을 보여주는, 저장소 규모의 검증된 소프트웨어 합성에 대한 진행 상황을 측정할 수 있는 구체적인 테스트 환경을 제공합니다. 벤치마크, 데이터 정제 파이프라인 및 평가 도구는 https://github.com/sunblaze-ucb/vero 에서 확인할 수 있습니다.

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.