Viverra: Text-to-Code with Guarantees

• URL: http://arxiv.org/abs/2605.14972v1
• Date: Thu, 14 May 2026 15:36:44 GMT
• Title: Viverra: Text-to-Code with Guarantees
• Abstract summary: Viverra is a system that automatically produces formally verified annotations alongside generated code to aid user's understanding of the generated program.<n>V Viverra can efficiently generate code with verified assertions, and that these assertions improve users' performance on code-comprehension tasks.
• Score: 5.566349423527438
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: A fundamental limitation of Text-to-Code is that no guarantee can be obtained about the correctness of the generated code. Therefore, to ensure its correctness, the generated code still has to be reviewed, tested, and maintained by developers. However, parsing through LLM-generated code can be tedious and time-consuming, potentially negating the productivity gains promised by AI-coding tools. To address this challenge, we present Viverra, a system that automatically produces formally verified annotations alongside generated code to aid user's understanding of the generated program. Given a natural-language task description, Viverra prompts an LLM to synthesize a C program together with candidate assertions expressing safety and correctness properties. It then verifies those assertions in a compositional and best-effort manner via a portfolio of bounded model checkers. Evaluation on 18 diverse programming tasks suggests that Viverra can efficiently generate code with verified assertions, and that these assertions improve users' performance on code-comprehension tasks in a user study with more than 400 participants.

Related papers

• Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming [18.004246438683147]
  Vibe coding democratizes software development by allowing users to generate code via natural-language (NL) interaction with large language models (LLMs)<n>This paper presents verifiable literate programming, a human-in-the-loop framework designed to make the review/validation process accessible to users at all programming levels.<n>The documentation demonstrates concrete program semantics and enables users to provide feedback on potential intent-code mismatches.
  arXiv  Detail & Related papers  (2026-07-02T15:37:54Z)
• CodeSimpleQA: Scaling Factuality in Code Large Language Models [55.705748501461294]
  We present CodeSimpleQA, a comprehensive benchmark designed to evaluate the factual accuracy of code LLMs in answering code-related questions.<n>We also create CodeSimpleQA-Instruct, a large-scale instruction corpus with 66M samples, and develop a post-training framework combining supervised fine-tuning and reinforcement learning.
  arXiv  Detail & Related papers  (2025-12-22T14:27:17Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• NoCode-bench: A Benchmark for Evaluating Natural Language-Driven Feature Addition [16.134058143793304]
  This work introduces NoCode-bench, a benchmark designed to evaluate large language models (LLMs) on real-world NL-driven feature addition tasks.<n>A subset of 114 high-quality, human-verified instances, NoCode-bench Verified, ensures reliable evaluation.<n>Our experiments reveal that, despite high token usage, the best LLMs achieve a task success rate of only 28.07%, highlighting challenges in cross-file editing, understanding, and tool calling.
  arXiv  Detail & Related papers  (2025-07-24T06:38:19Z)
• Towards Formal Verification of LLM-Generated Code from Natural Language Prompts [17.130884318613944]
  We seek to offer formal guarantees of correctness to LLM generated code.<n>We propose to incorporate a formal query language that can represent a user's intent in a formally defined but natural language-like manner.<n>Our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.
  arXiv  Detail & Related papers  (2025-07-17T16:54:42Z)
• Ensuring Functional Correctness of Large Code Models with Selective Generation [13.517414451760635]
  hallucination of code generation models hinders their applicability to systems requiring higher safety standards.<n>We propose emphselective code generator that abstains from uncertain generations based on functional correctness evaluated by generated unit tests.<n>We demonstrate the efficacy of our method along with the controllability of code hallucination and reasonable selection efficiency.
  arXiv  Detail & Related papers  (2025-05-19T06:29:16Z)
• NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
  We present NoviCode, a novel NL Programming task which takes as input an API and a natural language description by a novice non-programmer. We show that NoviCode is indeed a challenging task in the code synthesis domain, and that generating complex code from non-technical instructions goes beyond the current Text-to-Code paradigm.
  arXiv  Detail & Related papers  (2024-07-15T11:26:03Z)
• Chain of Targeted Verification Questions to Improve the Reliability of Code Generated by LLMs [10.510325069289324]
  We propose a self-refinement method aimed at improving the reliability of code generated by LLMs. Our approach is based on targeted Verification Questions (VQs) to identify potential bugs within the initial code. Our method attempts to repair these potential bugs by re-prompting the LLM with the targeted VQs and the initial code.
  arXiv  Detail & Related papers  (2024-05-22T19:02:50Z)
• Iterative Refinement of Project-Level Code Context for Precise Code Generation with Compiler Feedback [29.136378191436396]
  We present CoCoGen, a new code generation approach that uses compiler feedback to improve the LLM-generated code. CoCoGen first leverages static analysis to identify mismatches between the generated code and the project's context. It then iteratively aligns and fixes the identified errors using information extracted from the code repository.
  arXiv  Detail & Related papers  (2024-03-25T14:07:27Z)
• Test-Driven Development for Code Generation [0.850206009406913]
  Large Language Models (LLMs) have demonstrated significant capabilities in generating code snippets directly from problem statements. This paper investigates if and how Test-Driven Development (TDD) can be incorporated into AI-assisted code-generation processes.
  arXiv  Detail & Related papers  (2024-02-21T04:10:12Z)
• Code Prompting Elicits Conditional Reasoning Abilities in Text+Code LLMs [65.2379940117181]
  We introduce code prompting, a chain of prompts that transforms a natural language problem into code. We find that code prompting exhibits a high-performance boost for multiple LLMs. Our analysis of GPT 3.5 reveals that the code formatting of the input problem is essential for performance improvement.
  arXiv  Detail & Related papers  (2024-01-18T15:32:24Z)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  We propose ReCode, a comprehensive robustness evaluation benchmark for code generation models. We customize over 30 transformations specifically for code on docstrings, function and variable names, code syntax, and code format. With human annotators, we verified that over 90% of the perturbed prompts do not alter the semantic meaning of the original prompt.
  arXiv  Detail & Related papers  (2022-12-20T14:11:31Z)
• Python Code Generation by Asking Clarification Questions [57.63906360576212]
  In this work, we introduce a novel and more realistic setup for this task. We hypothesize that the under-specification of a natural language description can be resolved by asking clarification questions. We collect and introduce a new dataset named CodeClarQA containing pairs of natural language descriptions and code with created synthetic clarification questions and answers.
  arXiv  Detail & Related papers  (2022-12-19T22:08:36Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  Large language models (LLMs) produce code from informal natural language (NL) intent. It is hard to define a notion of correctness since natural language can be ambiguous and lacks a formal semantics. We describe a language-agnostic abstract algorithm and a concrete implementation TiCoder.
  arXiv  Detail & Related papers  (2022-08-11T17:41:08Z)

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.