Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover

• URL: http://arxiv.org/abs/2605.26017v1
• Date: Mon, 25 May 2026 16:35:36 GMT
• Title: Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
• Abstract summary: This paper studies whether interactive theorem provers (ITPs) can support large-scale software generation.<n>Because ITPs handle pure total functions but not effects such as I/O, our agent separates effectful code from pure logic.<n>We study this route through the fully automatic development of a CPU interpreter for all 47 instructions of the unprivileged RISC-V RV32I base.
• Score: 2.6146136791093104
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Generating code from natural-language requirements has become a primary route for LLM-assisted software development. Although LLMs can successfully complete small programming tasks, generating an entire complex project remains unreliable because subtle errors may survive compilation and testing. Verified programming can reduce this risk by requiring generated implementations to satisfy machine-checked specifications. Existing explorations mostly target verification-oriented languages and toolchains such as Dafny and Frama-C, but directly generating project-scale verified code with these systems remains difficult. This paper studies whether interactive theorem provers (ITPs) can support large-scale software generation. Because ITPs handle pure total functions but not effects such as I/O, our agent separates effectful code from pure logic: it implements the effects in the target language, proves the pure logic in an ITP, and extracts it for integration into the final project. We study this route through the fully automatic development of a CPU interpreter for all 47 instructions of the unprivileged RISC-V RV32I base: after the requirements are supplied, no human intervenes in synthesis, proof repair, extraction, or integration. With Rocq as the backend, the agent completes the project within 30 minutes, producing 1,859 lines of verified Rocq and extracting 2,848 lines of C++. The resulting interpreter passes all 265 LLM-generated tests covering the 47 instructions and exhibits zero crashes and zero hangs during 12 hours of AFL++ fuzzing. Under the same configuration, a Dafny-based backend fails to complete verification. Our observation is that Rocq exposes a concrete proof state when a proof attempt fails, giving the agent actionable feedback for repair. These results provide empirical evidence that ITP-based verified programming is a feasible route for LLM-generated software projects.

Related papers

• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  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.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizer is a framework that redirects hardware generation through a dependently-typed HDL embedded in Lean 4.<n>On VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems), CktFormalizer achieves simulation pass rates competitive with direct Verilog generation.
  arXiv  Detail & Related papers  (2026-05-08T14:20:06Z)
• ProgramBench: Can Language Models Rebuild Programs From Scratch? [59.40748183470308]
  ProgramBench measures the ability of software engineering agents to develop software holisitically.<n>End-to-end behavioral tests are generated via agent-driven fuzzing.<n>Models favor monolithic, single-file implementations that diverge sharply from human-written code.
  arXiv  Detail & Related papers  (2026-05-05T09:17:02Z)
• SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
  We introduce a neuro-symbolic, scenario-based framework that bridges the gap between high-level program intent and the rigid syntactic constraints of pointer arithmetic and manual memory management.<n>We evaluate it on 59 real-world and algorithmic subjects, where it outperforms the vanilla prompt generation baseline by 31.36% in line coverage, 26.01% in branch coverage, and 20.78% in mutation score, matching or exceeding the symbolic execution tool KLEE.
  arXiv  Detail & Related papers  (2026-02-18T18:09:03Z)
• Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
  Generative Logic (GL) is a deterministic architecture that starts from usersupplied axiomatic definitions.<n>GL enumerates conjectures, applies normalization, type, and CE filter, and automatically reconstructs machine-checkable proofs.
  arXiv  Detail & Related papers  (2025-07-25T17:29:19Z)
• PRO-V: An Efficient Program Generation Multi-Agent System for Automatic RTL Verification [6.983135183126461]
  Pro-V is a fully program generation multi-agent system for robust RTL verification.<n>It incorporates an efficient best-of-n iterative sampling strategy to enhance the correctness of generated testbenches.<n>Pro-V attains a verification accuracy of 87.17% on golden RTL implementations and 76.28% on RTL mutants.
  arXiv  Detail & Related papers  (2025-06-13T20:06:34Z)
• Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
  We propose a novel framework that leverages functional programming and type systems to translate backend code into formal Lean representations.<n>Our pipeline automatically generates theorems that specify the intended behavior of APIs and database operations, and uses LLM-based provers to verify them.<n>We evaluate our method on realistic backend systems and find that it can formally verify over 50% of the test requirements, which suggests that half of a testing engineer's workload can be automated.
  arXiv  Detail & Related papers  (2025-04-13T16:49:37Z)
• BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions [72.56339136017759]
  We introduce BigCodeBench, a benchmark that challenges Large Language Models (LLMs) to invoke multiple function calls as tools from 139 libraries and 7 domains for 1,140 fine-grained tasks.<n>Our evaluation shows that LLMs are not yet capable of following complex instructions to use function calls precisely, with scores up to 60%, significantly lower than the human performance of 97%.<n>We propose a natural-language-oriented variant of BigCodeBench, BigCodeBench-Instruct, that automatically transforms the original docstrings into short instructions only with essential information.
  arXiv  Detail & Related papers  (2024-06-22T15:52:04Z)
• Get my drift? Catching LLM Task Drift with Activation Deltas [55.75645403965326]
  Task drift allows attackers to exfiltrate data or influence the LLM's output for other users.<n>We show that a simple linear classifier can detect drift with near-perfect ROC AUC on an out-of-distribution test set.<n>We observe that this approach generalizes surprisingly well to unseen task domains, such as prompt injections, jailbreaks, and malicious instructions.
  arXiv  Detail & Related papers  (2024-06-02T16:53:21Z)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Bench is a benchmark rooted in real-world programming applications that leverage existing code repositories to perform tasks. To evaluate both Large Language Models (LLMs) and AI agents, two setups are employed: ML-LLM-Bench for assessing LLMs' text-to-code conversion within a predefined deployment environment, and ML-Agent-Bench for testing autonomous agents in an end-to-end task execution within a Linux sandbox environment.
  arXiv  Detail & Related papers  (2023-11-16T12:03:21Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  We propose LEVER, a simple approach to improve language-to-code generation by learning to verify the generated programs with their execution results. Specifically, we train verifiers to determine whether a program sampled from the LLMs is correct or not based on the natural language input, the program itself and its execution results. LEVER consistently improves over the base code LLMs(4.6% to 10.9% with code-davinci) and achieves new state-of-the-art results on all of them.
  arXiv  Detail & Related papers  (2023-02-16T18:23:22Z)

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.