Source-linked AI summary
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
Shuvendu K. Lahiri
TL;DR
Mainstream developers often lack verification support, while specifying program properties and environments requires formal-methods expertise. NFV combines AI coding agents with established verifiers to produce machine-checked verdicts, reaching 57% coverage at 92% precision on a challenging dataset and motivating empirical evaluation of formal reasoning tools.
Problem
Mainstream languages have limited verification support, and specifying properties and execution environments requires formal-methods expertise, so shipped code is commonly assured through review and testing.
Method
NFV uses an AI coding agent to translate mainstream-language programs and specifications into verification-aware artifacts, while an established verifier decides correctness or refutation.
Results
57% of the dataset received a machine-checked verdict at 92% precision, while the remaining 43% lacked a proof.
Takeaways & Limitations
Treating formal program reasoning as an empirical accuracy problem makes it measurable across models and amenable to improvement methods for learned components.
Takeaways & Limitations
Bounded-search failures can be spurious when the environment is under-constrained, whereas proof of refutation guarantees a bug only under the stated environment assumptions.
Abstract
from arXiv · showhide
Formal verification offers the strongest assurance available for software, and verification-aware languages have made its automation real. Yet the benefits reach few mainstream developers, most of whose languages have no verification support. Besides, specifying properties and modeling the environment require expertise in formal methods. Proof is therefore reserved for a few celebrated artifacts, while the production code that ships is attested only through review and testing. We introduce neuro-formal verification (NFV), which harnesses that automation for developers of mainstream programming languages: an AI coding agent translates, an established verifier decides, and a question posed in a mainstream language is answered push-button, at empirical accuracy rather than soundness, with a machine-checked proof. Results on a dataset of correct and incorrect solutions to Python programming problems are encouraging: NFV returns a Dafny proof of correctness or of a bug on 57% of the entries at 92% precision, and a CBMC counterexample for 63% of the buggy programs at 90% precision.
1 Introduction
Formal verification provides strong assurance but remains difficult for mainstream developers because language formalization and environment modeling require specialized expertise. NFV addresses this gap by combining AI translation with mature verifiers to deliver empirical, push-button, machine-checked reasoning results.
- Motivation: Formal verification derives mathematical proofs of program properties, but successful deployments remain relatively few and often require experts in verification systems.Mature systems such as Dafny, F*, Verus, Lean, Rocq, and Isabelle/HOL combine automation with user-supplied proof structure.
- Motivation: Mainstream-language verification must formalize language constructs and model the execution environment, including libraries, external state, and unstated preconditions.Different C verifiers already embody different memory models, specification formalisms, and proof systems.
- Motivation: AI coding agents increase the demand for assurance while also becoming capable of writing code and proofs in verification-aware languages.The paper identifies this combination as changing the feasibility of bringing formal reasoning to mainstream development.
- Neuro-formal verification: NFV translates mainstream-language programs and specifications into a mature formal language, uses agentic proof search checked by a verifier, and maps successful proofs back to developer-facing sketches.The workflow includes intent formalization, program and specification translation, proof search, and proof mapping.
2 Dataset
The dataset builds a curated benchmark of correct and buggy Python implementations paired with synthesized specifications, then characterizes programs by library use, size, and control flow. Conservative filtering leaves a corpus intended for empirical neuro-formal verification, while its small scale limits conclusions about program scale.
- Source: The dataset extends HumanEval with natural-language docstrings, reference implementations, synthesized postconditions, and mutants that fail tests.
- Filtering: Conservative filtering removes references that violate their specifications and tasks whose tests do not complete, leaving 116 task pairs.
- Tiers: Library tiers L0–L3 proxy how much environment formalization is needed, ranging from arithmetic and control flow to external modules or calls.
- Size: Mutants are longer than references on 73 of 103 tasks and shorter on 18, with a median paired difference of 2 lines.
- Size: The programs are small, with most containing loops and branches, so benchmark results do not establish performance at scale.
3 Neuro-formal verification (NFV)
NFV translates mainstream-language programs and specifications into a verification-aware language, then uses agentic proof search and established verifiers to produce correctness proofs or refutations. The proof-based and bounded pipelines share goals but differ in scalability, inspectability, completeness, and failure modes.
- 3.1 The proof-based pipeline: The proof-based pipeline formalizes libraries and preconditions, transliterates the program, renders the specification, and performs agent-driven proof search and repair.Library theory and preconditions freeze before the goal is visible; proof search may synthesize invariants, lemmas, and intermediate assertions.
- 3 Neuro-formal verification (NFV): NFV instantiates a framework with Python as source language and Dafny as verification target, while aiming for broader language and backend applicability.The concepts are described as applicable to languages such as C#, Java, and JavaScript and backends such as F⋆ and Lean.
- 3.1.1 Verification proof: Provenance tags tie translated lines to source code or synthesized declarations, while frozen artifacts and mechanical checks prevent proof search from altering the verification task.The pipeline rejects untagged code and re-checks frozen source, environment theory, preconditions, and goals on repair rounds.
- 3.1.2 Refutation proof: Refutation negates the postcondition, has the agent propose a violating input, installs it as a precondition, and proves that the unchanged program violates the specification.Reachability and goal-shape checks ensure that the witness is used to establish a genuine refutation rather than merely report proof failure.
- 3.2 The bounded-verification-based pipeline: The bounded-verification arm uses CBMC-like search for an execution violating the goal within a fixed unwinding; a violating trace refutes, while other outcomes abstain.Unlike the proof-based arm, it does not repair proof failures and searches directly for a witness.
- 3.3 Proof-based versus bounded verification for refutation: Proof-based refutation can scale modularly and is easier to inspect because provenance maps proof vocabulary back to source lines, whereas long interprocedural traces can be difficult to act on.Bounded verification is described as inherently non-scalable with call-chain depth, while proof inspection benefits from source-level provenance.
- 3.3 Proof-based versus bounded verification for refutation: Neither refutation approach is complete: proof-based refutation misses bugs dependent on internal nondeterminism, while bounded failures may be spurious under under-constrained environments.A proof of refutation, when present, guarantees a bug under the stated environment assumptions.
4 Evaluation
Across the Dafny evaluation, NFV combines verification and refutation into a proof-producing pipeline, while incorrect verdicts primarily reflect specification assumptions, translation choices, or library formalization.
- Dafny evaluation: ≈70% recall and ≈93.5% precision characterized verification, which proved 72 of 103 correct references and 5 incorrect mutants.
- Dafny evaluation: 57.3% recall and 92.2% precision were achieved by the combined pipeline, which issued proofs for 128 of 206 tasks.Its overall F1 score was 0.71.
- Dafny evaluation: NFV struggled most in L3 because imported libraries were hard to model, whereas wrong verdicts traced to unstated preconditions and chosen argument types.
- Error analysis: All six counterexamples against references were real Python counterexamples to the written postcondition, caused by missing preconditions.
- Error analysis: Three of five spurious proofs were valid only under stronger preconditions, including inferred input restrictions and an incorrect translated type signature.
- Error analysis: One false proof copied a mutant’s buggy loop into the translated library specification, making the obligation reproduce the same error.
- Error analysis: One incorrect label arose because EvalPlus added a negative-integer test violating the docstring’s stated non-negative-input precondition.
4.3 The bounded-verifier arm: CBMC
The CBMC arm translates library documentation into C and uses bounded verification to refute buggy programs while checking for undefined behavior.
- CBMC setup: The translated C must compile and be free of undefined behavior, including overflow, bounds, pointer, and conversion violations.
- CBMC evaluation: 63% recall and 90% precision were obtained when CBMC issued 72 counterexamples, including 65 true mutant refutations and 7 false ones.On the same programs, Dafny refutation reached 46% recall and 89% precision.
- CBMC evaluation: CBMC’s bounded verification provides an alternative refutation path when bounded verification can scale, with preconditions again the dominant source of unsound refutations.
4.4 Weaker LLMs
NFV’s performance depends strongly on the language model: the strongest model retained useful precision and recall, while weaker models degraded asymmetrically across tasks.
- Model comparison: Around 90% precision and around 58% recall were achieved only by gpt-5.6-sol on this dataset.
- Model comparison: claude-haiku-4.5 performed poorly on both tasks and had the most typechecking or audit failures among the compared models.
- Model comparison: Refutation was the resilient direction, while weaker models showed a sharp verification decline through reduced recall, reduced precision, or both.
4.5 Strawman and symbolic baselines
NFV outperformed a direct LLM judge in precision and avoided the unsound incentives of a verifier-only baseline, while symbolic verification was limited by missing type annotations.
- Baseline design: The baselines span a spectrum from fully neural to fully symbolic, positioning NFV between direct judgment and standalone verification.
- Neural baseline: 72% precision was achieved by the always-committing LLM judge, versus 92% for NFV, which abstains without a proof artifact.
- Verifier baseline: 98% of correct and 98% of known-wrong programs were proved by LLM+verifier, but precision was only 50% because 57% of unsound proofs rewrote the program or specification.
- Symbolic baseline: Nagini proved 0% by default because 83% of entries lacked type-annotated signatures, although agent-supplied annotations increased the fraction reaching verification.
5 Related work
NFV builds on symbolic verification, translation-based checking, environment modeling, and recent AI-agent advances to extend formal reasoning across mainstream languages.
- Translation-based verifiers compile programs into intermediate verification languages and then use SMT solving.
- Extended-static checkers analyze formal source models while sometimes trading soundness for broader code coverage.
- Open programs require environment modeling, leaving end-to-end soundness to user assumptions or heuristic inference.
- NFV proposes leveraging AI agents in language-agnostic formal reasoning for mainstream developers.
- Its supporting directions include neural translation, intent formalization, and agentic proof automation.These directions draw on translation datasets, symbolic validation against tests, and advances in invariant and proof generation.
6 Conclusion and Future Work
The paper presents NFV as an integration of AI coding agents with verification-aware languages and reports encouraging machine-checked coverage, while identifying substantial work needed for realistic deployment.
- 57% of the dataset received a machine-checked verdict at 92% precision.The remaining 43% received no proof from the current flagship model.
- NFV integrates AI coding agents and verification-aware languages to support language-agnostic formal program reasoning.
- Future evaluations should cover representative real-world tasks, richer libraries, concurrency, intent formalization, environment specifications, and realistic user studies.The paper also calls for symbolic techniques and benchmarks to improve trustworthiness and evaluate generated specifications.
- Treating formal reasoning as empirical accuracy rather than a Boolean soundness question makes it measurable across models and improvable through learned-component methods.
A.1 The benchmark in full
The benchmark contains 103 task pairs, totaling 206 reference and mutant entries, each evaluated against a shared postcondition and linked to upstream identifiers.
- Table 7 lists every task in nl2post-safe together with its scored postcondition and upstream identifiers.
- 103 pairs comprise all 206 benchmark entries, with each pair scored against a postcondition.
- Mutant identifiers below 200 denote natural mutants, whereas identifiers from 200 onward denote artificial mutants.
- The reference and mutant for each task share the same postcondition.
- Listed tasks span operations including rolling maxima, palindrome construction, string XOR, greatest common divisor, digit sums, filtering, histograms, and ordering.
B An example program from each library tier
The library tiers illustrate increasing specification demands, from self-contained arithmetic and control flow to external APIs, collection relations, and quantified higher-order behavior.
- L0 — HumanEval/157: L0 uses only arithmetic, indexing, and control flow, so its trusted base can be empty.
- L1 — HumanEval/121: L1 adds sum while retaining self-contained total functions whose meanings can be stated directly.
- L2a — HumanEval/120: L2a uses sort operations and requires specifications relating whole collections, including their contents and order.
- L2b — HumanEval/30: L2b uses filter and requires quantification over an argument whose function body is unavailable.
- L3 — HumanEval/133: L3 imports math, map, math.ceil, and sum, requiring axioms for an externally defined surface that remain assumed rather than checked.