arXiv CS open access

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

2026 · arxiv_cs

arXiv CS · Papers · 2026

software-architecture software-engineering testing

Conceptio Open Archive

Analyze & explore related research in Conceptio

Connect this record directly into your research workflow or AI agent. Explore citations across open repositories, query full text, and export structured proof bundles.

Explore in Search →Connect via MCP / API ↗

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

arXiv:2608.21516v1 [cs.SE] 21 Aug 2026

Shuvendu K. Lahiri Microsoft Research Abstract Formal verification offers the strongest assurance available for software, and verificationaware 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 compared to an llm-as-judge baseline: 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.

Introduction

Formal program verification refers to the use of mathematical logic to derive a mathematical proof of a formal property ϕ against a formal model of a program P operating in an execution environment E. The idea dates to Turing [1] and Hoare [2], and it has been held out ever since as the strongest available form of assurance for program correctness. Decades of work have made it real. A range of mature verification-aware languages and proof assistants — Dafny [43], F⋆ [9], Verus [15], Lean [3], Rocq [7], Isabelle/HOL [8] — combine SMT-backed [5, 6] automation with usersupplied proof structure in varying proportions, and serious systems have been proved correct in them [10, 11, 12, 13]. Such success stories are, however, countable and often the work of experts in those systems: green-field projects in which code and proof are co-developed, under a methodology that takes years to establish. A proof of ϕ for a program P in a mainstream language L faces two additional obstacles. First, L’s constructs must be formalized — in a program logic or an intermediate verification language (IVL) such as Boogie [16]. Efforts in that direction, from VCC [14] to Verus [15], are real but slow and cover a handful of languages; even for a language as studied as C there is no single verifier for the whole language, as CBMC [37], VCC and Frama-C [36] embody different memory models, specification formalisms and proof systems, each catering to a different appetite for automation. Second, a proof about P is a proof about P running in an environment E — the precondition the developer has in mind, the semantics of the libraries P calls, the external state it reads and updates — all of which has to be inferred from documentation and world knowledge. The SLAM/SDV developers, for instance, spent decades building and maintaining accurate models of the operating 1

system in order to verify device drivers against it [39]. As a result, for the code that actually ships, developers have stuck with code review and testing as the cost-effective way to obtain assurance. Two developments of the past year change the calculation. First, a large and growing share of code is “vibe-coded” [35] by AI coding agents rather than by people, which raises the demand for assurance. Second, those same agents turn out to be unexpectedly good at writing code and proofs in exactly the verification-aware languages whose expert supply has long been a bottleneck [40, 41, 4]. This motivates the question this paper sets out to answer: Can we harness the proof automation of the mature verification-aware languages, for mainstream developers, in a language-agnostic way? In this paper, we describe neuro-formal verification (NFV), as one possible answer to the above question. An effective neuro-formal verifier would provide a developer in a mainstream programming language L the ability to pose formal reasoning questions (say, expressed as a formal assertion in L) and obtain an answer with (a) high empirical accuracy — accuracy, not soundness, (b) in a push-button manner (as the default mode), and (c) a sketch of a formal proof artifact. We hypothesize that such a tool can be invaluable for developers to audit, understand and gain trust in code, especially when AI-generated.

1.1

Neuro-formal verification: the whole picture

The inputs. A developer has a program PL in some source language L; a property Snl they care about, written in whatever notation they already use — a docstring, an issue, a comment; and an environment E their program calls into, described the way environments actually are: documentation Enl . The workflow. Figure 1 lays out five stages that turn those inputs into a checked proof and hand it back in the developer’s own terms. 1. Intent formalization [47]. Synthesize the formal specification EF from Enl — the contracts of the libraries the program calls, and any precondition the documentation states, stated in F — and SL from Snl , an assertion in the source language meaning what the developer meant. Both are claims about intent, and both should be attested against every artifact available — the documentation, the tests, and the source where there is source. 2. Program translation, PL → PF , into the formal language F of some mature verifier. This step can range from purely symbolic (a compiler, where a faithful front end exists) through mixed to purely neural (this paper). 3. Specification translation, SL → SF , along the same spectrum. 4. Proof search over F , discharged by the verifier for F and driven agentically: an agent proposes invariants, lemmas and tactics, the verifier checks every one, so the search may be as neural as it likes without putting soundness at risk. 5. Proof mapping. Carry a successful Proof (PF , SF , EF ) back to PL as a proof sketch: the proof restated over the developer’s own variables, the assumptions named in terms of Enl . Note that the above workflow should not be construed as formal verification of SL against PL executing within Enl , partly because the problem is not formally stated at the level of L. We use the term formal program reasoning instead. 2

formal verification 1

Enl

agentic search

intent formalization

docs, tests, source

invariants, lemmas, tactics proposals / failures

Snl

intent formalization

docstring

neuro-symbolic translator

proof search

Proof F

verifier for F

PL source program

purely symbolic → mixed → purely neural

developer

informal

in L

in F

rounded box = a step, tape = an artefact

proof mapping

proof sketch over PL + verdict

Figure 1: Neuro-formal verification. Circled numbers are the five stages enumerated above. Rounded boxes transform; tape-shaped nodes are the artifacts they consume and produce, colored by the language the artifact lives in — orange for informal English, gray for the source language L, purple for the formal language F . Blue is a step an LLM performs, green a step a verifier performs. The developer authors Snl and PL and reads the proof sketch that comes back. The dashed red region is the classical formal verification problem — given PF , SF and EF , find a proof.

An example.

Let us illustrate the workflow for this paper with a simple two-line Python program:

def shifted_mean(l): "Average the list after adding 1 to each element; l must be non-empty." return sum(x + 1 for x in l) / len(l) # postcondition assert shifted_mean(l) == sum(l) / len(l) + 1

Informally, the correctness of this specification relies on len(l) ̸= 0 and sum( {x + 1 | x ∈ l} ) = sum(l) + len(l). Stage 5 would not only return “verified” but also the reason, in natural language: the specification holds because adding 1 to each of len(l) elements adds len(l) to their sum, provided the list is non-empty — an artifact the developer can check. The same example, worked in Dafny. Instantiating F with Dafny makes the workflow concrete. Stage 1 starts from Enl , which for this program is the documentation of Python’s sum1 — all that is actually on offer about the library: Return the sum of a ’start’ value (default: 0) plus an iterable of numbers. When the iterable is empty, return the start value. 1

The built-in’s runtime docstring — sum. doc restricting it to numeric values.

in CPython 3.14 — quoted as it stands, less a closing sentence

The EF it becomes is a recursive definition and the induction the second fact needs; nothing here mentions shifted mean: function Sum(l: seq<real>): real { if |l| == 0 then 0.0 else l[0] + Sum(l[1..]) } function Shift(l: seq<real>): seq<real> { seq(|l|, i requires 0 <= i < |l| => l[i] + 1.0) } lemma ShiftedSum(l: seq<real>) ensures Sum(Shift(l)) == Sum(l) + |l| as real { if |l| > 0 { assert Shift(l)[1..] == Shift(l[1..]); ShiftedSum(l[1..]); } }

Sum is the attestable part: it is a definition, it terminates, and one can read it against the docstring. ShiftedSum is that second fact, but stated as a lemma with a proof — a one-line induction the verifier checks. Stages 2 and 3 then render PF and SF straightforwardly: method ShiftedMean(l: seq<real>) returns (r: real) requires |l| > 0 ensures r == Sum(l) / (|l| as real) + 1.0 { ShiftedSum(l); var n := |l| as real; r := Sum(Shift(l)) / n; DivDistrib(Sum(l), n); }

The last call is the stage-4 lesson. Even with EF in hand the verifier does not close the goal: it knows Sum(Shift(l)) = Sum(l) + n but will not divide through, because n is symbolic and (a + n)/n = a/n + 1 is nonlinear. What the proof search must find is a second lemma, and the proof of it is again two asserts the verifier can check (n/n = 1, and division distributing over the sum): lemma DivDistrib(a: real, n: real) requires n != 0.0 ensures (a + n) / n == a / n + 1.0 { assert n / n == 1.0; assert (a + n) / n == a / n + n / n; }

Dafny discharges all seven obligations of the resulting file. The same example with a bug, refuted. Suppose the developer had written the reduction as a single addition on the total rather than one per element — r := (Sum(l) + 1.0) / n in place of r := Sum(Shift(l)) / n, a one-token slip. Now PF does not meet SF , and stage 5 should say so. The tempting move is to report the verifier’s failure: Dafny cannot prove the postcondition. However, a proof failure cannot be interpreted as a bug — an unproved goal is evidence about the proof search, not about the program. What makes a refutation attestable is the same thing that makes a verification attestable — a proof that SF fails. The program is left untouched, SF is negated, and the witness is added as a precondition, so the verifier is asked to confirm a positive claim rather than to fail at a negative one:

method ShiftedMean(l: seq<real>) returns (r: real) requires |l| > 0 requires l == [0.0, 0.0] // the witness ensures !(r == Sum(l) / (|l| as real) + 1.0) // S_F, negated { var n := |l| as real; r := (Sum(l) + 1.0) / n; // the bug assert Sum(l) == l[0] + Sum(l[1..]); assert Sum(l[1..]) == l[1] + Sum(l[1..][1..]); assert l[1..][1..] == []; }

The witness l = [0, 0] makes the buggy program return 1/2 where SF demands 1; the three asserts are the proof-repair loop unfolding Sum on that input, and Dafny discharges the negated goal.

1.2

Contributions of this paper

We develop a dataset, take one path through Figure 1, and measure it empirically. We begin at SL , since our benchmark supplies the assertion synthesized from a docstring by prior work [46]. Similarly, we synthesize EF but do not attest it formally against tests describing Enl . We sit at the neural end of the translation spectrum throughout. And we stop at a verdict carrying a machine-checked proof in F rather than a sketch of it over PL — evaluating it requires a careful user study. We study NFV empirically, and to make that possible we contribute: • A dataset of 206 Python (program, specification) pairs — 103 correct references and 103 buggy mutants of them — derived from prior work. • The NFV framework itself, its goal-blind staged discipline and the gates/checks that enforce it, together with two instances, one proof-based and one based on a bounded-program verifier. • Instantiating the framework with Dafny for proofs and CBMC for bounded verification. With those in place we demonstrate encouraging and timely results: • With a flagship frontier model, – the Dafny backend proves 70% of the correct programs and refutes 46% of the mutants at 94% and 89% precision, signifying the viability of the approach. – CBMC refutes 63% of the mutants at 90% precision — the highest recall and precision for finding bugs in this dataset. – On this dataset, a majority of incorrect verdicts stem from incorrect precondition synthesis in EF that can improve with better intent-formalization methods; other components may be no less error-prone on other workloads. • Less capable frontier models perform significantly worse on both verification and refutation — this capability may not have existed even a year ago. • NFV outperforms the strawman LLM-as-a-judge baseline on this dataset: the judge answers every entry at 72% precision (compared to the 92% precision NFV provides through its ability to abstain when it cannot back its verdict with a proof artifact). A dual reading. We have described the architecture from the verification side: a formal method that uses an LLM as its front end. It reads equally well from the other side, as equipping an AI agent with a formal verifier : the LLM is the agent, the pipeline is a tool it calls to discharge a claim about program correctness.

Organization. Section 2 describes the dataset, Section 3 the framework, and Sections 4 and 4.2.1 the experiments and the errors that remain.2

Dataset

This section describes a dataset we curate to study neuro-formal verification empirically.

2.1

Curation

Source. We select the programs and specifications from the nl2postcond benchmark [46].3 This dataset builds on the HumanEval [44] dataset, each task of which provides (i) a naturallanguage docstring stating the intended behavior of the function, together with a handful of worked input/output examples, and (ii) a reference Python implementation P , taken to be correct with respect to a set of tests T augmented by EvalPlus [45]; and augments it with (iii) a set of postconditions synthesized from the task docstring and (iv) a set of mutants M that fail the tests. Each postcondition is labeled sound if it passes each test in T over P ; its completeness is the fraction of M killed by running the test inputs in T with the postcondition asserted. We take the postconditions from that repository’s eval_results/gpt4_simple_no_ref.zip — the GPT4 SimplePromptNoRef arm, whose summary_eval_results.jsonl carries the soundness and completeness verdicts and whose individual_postcondition_results/ directory carries one file per candidate — and the mutants together with their killing inputs from eval_results/distinct_ code_mutants.jsonl.zip. Initial pool. For each task, we choose the specification that has the highest completeness score. Next, we choose the first mutant that the specification is confirmed to kill on an input in T . This provides us with 155 reference implementations (labeled correct) and 155 mutant implementations (labeled incorrect), where each pair shares a specification S. Filtering. We then apply two filters. The first checks whether the reference fails the specification — the goal is to remove any example where the specification is incorrect, assuming the reference implementation is correct. claude-sonnet-4.5 was prompted for 100 diverse inputs per task and these were executed against P and S over all 155 references. We dropped 6 tasks where P was observed to violate S, and 33 more whose tests did not run to completion, leaving 116. Our approach is conservative — the falsifying input may itself violate a precondition the docstring states only in prose. The second filter drops 13 tasks whose postcondition constrains only the return type, an obligation that a typed target language encodes in the method signature and that therefore does not exercise the program verifier. What remains is 206 entries over 103 tasks, balanced by construction. Appendix A.1 lists every one of them with the postcondition it is scored against and the upstream identifiers that pin it, so the corpus can be reconstructed without rerunning the one filtering step that is not deterministic.

2.2

Characteristics

Tables 1 and 2 characterize the resulting corpus along two axes: the library surface each program uses, and its size and control flow. Tiers. Table 1 splits the corpus by library tier L0–L3, a function of the calls the Python source makes: a proxy for how much the LLM must formalize the environment, not for algorithmic 2

The dataset, the pipeline and the scripts that produce every table and number reported here will be released shortly as open source. 3 https://github.com/microsoft/intent-formalization/tree/main/nl2postcondition-fse2024

Table 1: nl2post-safe by library tier. Tier

What the program touches

L0 L1 L2a L2b L3

nothing to axiomatize total built-ins only collections, first-order only a function passed as an argument module imports, unmodeled built-ins

All

Tasks

Entries

21 22 25 26 9

42 44 50 52 18

20% 21% 24% 25% 9%

103

206

100%

Table 2: Size and control flow of the 206 programs. LOC counts distinct physical lines of the function under test carrying a syntax node; comments, blank lines, imports and the docstring are excluded. Paired by task, mutants are longer than their reference on 73 of 103 tasks and shorter on 18, a median gap of 2 lines. min

p25

median

mean

p75

p90

max

7.6

LOC control flow

loop-free ≥ 1 loop ≥ 2 loops

92 114 24

45% 55% 12%

control flow

≥ 1 branch ≥ 1 comprehension

144 37

70% 18%

difficulty. L0 needs no axiom at all — arithmetic, indexing, control flow, len, range; L1 adds total built-ins (abs, sum, ord); L2a is first-order collection use; L2b passes a function as an argument, so the specification must quantify over a body it cannot see; L3 is a module import or any call outside these. Appendix B shows an example of each. Size. Table 2 gives program size and control flow: small programs, a majority of them containing a loop and most a branch, so no result here is evidence about scale. The mutants are independently written solutions rather than minimal edits and are often longer than their references.

Neuro-formal verification (NFV)

This section instantiates the neuro-formal verification framework (Figure 1) by elaborating some of the components. First, we describe some syntactic safeguards to ensure that the AI agent does not simplify or alter the verification task midway through the pipeline (e.g., changing the translated source PF during neural proof search); these are collected in Section 3.1.1. Second, we describe how to adapt the framework to perform a proof of refutation of the specification SF (Section 3.1.2). Finally, we also extend the framework to accommodate bounded-program verifiers (such as CBMC or Corral) that search for witnesses over bounded unrolling of the program loops and recursion (Section 3.2).

3.1

The proof-based pipeline

We outline both the verification and refutation arms of this pipeline. Both directions roughly run the same sequence of steps and hand the result to a deductive verifier; they differ only in the goal. The steps refine the stages of Figure 1: the library theory (stage 1a) and the precondition (stage 1b)

are the two halves of EF produced by stage 1; transliterating the body is stage 2; rendering the specification is stage 3; and proof search and repair are stage 4. We instantiate the framework with a specific choice of L (Python) and F (Dafny), but the concepts should be broadly applicable to other programming languages (C#, Java, JavaScript) and verifier backends (F⋆ , Lean). We choose Dafny as our target verification-aware language for this work since it supports many features of modern imperative programming languages such as sequences and so lets the translation stay close to the source. 3.1.1

Verification proof

The verification arm aims to produce a proof of SL over a translated program. Stage 1a formalizes the Python library surface the program touches and stage 1b synthesizes preconditions from the docstring; both freeze before the specification is visible, so neither the library theory nor the precondition can be chosen to suit the goal. Provenance tags. Stage 2 tags every emitted line with either src:, quoting its Python line verbatim, or synth:, marking it as having no source counterpart (declarations, invariants, decreases clauses). Untagged code is rejected — without that rule, rewritten logic hides in lines the audit cannot see. Translation has its own repair loop, but the only feedback is to run a syntax checker (e.g., dafny resolve in Dafny): type and resolution errors. The loop sees no verifier goal, so it has no information with which to make the program correct, only enough to make it well-formed. Figure 2 shows the partial artifact for our running example. Every line carries a provenance tag, and the two src: lines quote the Python verbatim. Sum is the only stage-1a content here: what Python’s sum means, written before the goal is visible. Frozen marks what proof search may not change — every src: line, the stage-1a theory, the stage-1b precondition and the goal itself — each re-checked mechanically on every repair round; the lemmas and the two proof calls at the bottom are what the repair loop contributed. Shift encodes the generator expression and so belongs to the translation that calls it. ShiftedSum and DivDistrib are the output of proof search — the facts the goal reduces to, found from the verifier’s failures — and both are lemmas proved in the target rather than assumed. The full artifact verifies at seven obligations. In addition to the above checks to ensure the translated code and environmental specifications are not altered to achieve a proof, we also ensure that the precondition is not inconsistent and the translation does not introduce unproven assumptions. 3.1.2

Refutation proof

Refutation asks the opposite question — is there an input class on which the specification provably breaks — and reuses stages 1a, 1b and 2 byte-identically. The goal is negated mechanically, the postcondition SF becomes ¬SF . Next, the LLM proposes a violating input looking at only the Python source; that guess is installed as an additional precondition (this is an exception to the verification arm, where preconditions cannot be strengthened); and proof repair proves the negated goal with the body still frozen. Similar to the verification proof, this may require the synthesis of invariants, lemmas and intermediate assertions. We also check a few additional facts specific to refutation. Reachability requires that replacing the postcondition with false fails verification. Goal shape requires that only the inversion of SF is present as a postcondition.

Python + specification def shifted_mean(l): "Average the list after adding 1 to each element; l must be non-empty." return sum(x + 1 for x in l) / len(l) assert return_value == sum(l)/len(l) + 1

Translated Dafny artifact // synth: frozen library theory // doc: sum(iterable, start=0) returns start plus the // items of the iterable; on an empty iterable, start. function Sum(l: seq<real>): real { if |l| == 0 then 0.0 else l[0] + Sum(l[1..]) } // synth: translation helper, for the generator expression function Shift(l: seq<real>): seq<real> { seq(|l|, i requires 0 <= i < |l| => l[i] + 1.0) } // synth: proof, proved not assumed lemma ShiftedSum(l: seq<real>) ensures Sum(Shift(l)) == Sum(l) + |l| as real { /* induction on l */ } lemma DivDistrib(a: real, n: real) requires n != 0.0 ensures (a + n) / n == a / n + 1.0 { /* two asserts, both checked */ } // src: source.py:1 | def shifted_mean(l): method shifted_mean(l: seq<real>) returns (return_value: real) // synth: frozen precondition, from "non-empty" requires |l| > 0 // synth: frozen postcondition ensures return_value == Sum(l) / (|l| as real) + 1.0 { // src: source.py:3 | return sum(x + 1 for x in l) / len(l) return_value := Sum(Shift(l)) / (|l| as real); // synth: proof ShiftedSum(l); DivDistrib(Sum(l), |l| as real); }

Figure 2: The running example of Section 1.1 as the pipeline emits it. The bodies of ShiftedSum and DivDistrib are elided for space; both are proved, and Section 1.1 gives those proofs.

3.2

The bounded-verification-based pipeline

The second instantiation drops the proof and searches for the witness directly. It shares most of the stages, except that they address only refutation. A bounded model checker (such as CBMC, which operates over C) answers the refutation question natively: it searches for an execution violating the goal assertion within a fixed unwinding, so a violating trace is a refutation and every other outcome, including a clean run, is an abstention. This arm also has no counterpart of repairing proof failures.

3.3

Proof-based versus bounded verification for refutation

Both pipelines can refute a program: the proof-based one by proving that a witnessing precondition forces a violation, the bounded one by finding a trace that exhibits it. Neither is complete, and the challenges each faces are different.4 Proof scales; search enumerates. A refutation (proof) search can scale to large modules due to its modular nature when paired with an effective (agentic) proof search automation. On the other hand, bounded verification is inherently non-scalable and is known to deteriorate with the depth of 4

We assume throughout that we cannot simply run P instead. Executing P may be unavailable or not costeffective — P may be a component of a larger system (say a device driver) needing hardware, a build or a fixture the auditing tool does not have — or ϕ may speak of ghost state with no runtime representation.

Table 3: Dafny, the reference backend, on each task and its own population. Verification and refutation run at 5 attempts × 10 proof rounds. The pipeline row is composed from the two arms above — refutation first, verification on what it leaves open — so every row is the same backend. “wrong” counts verdicts contradicting the label. task

population

issued

wrong

prec. (%)

rec. (%)

verification (P |= S) refutation (P ̸|= S)

103 103

77 53

5 6

93.5 88.7

69.9 45.6

0.80 0.60

pipeline (refute, then verify)

206

128

92.2

57.3

0.71

call chains. Ideas such as stratified inlining [52], that keeps callees abstract until a candidate trace demands them, may offer some relief — but cannot help with indefinite scaling. Proof is easier to inspect. A proof is written in the vocabulary of the translated program, so the provenance tags map it back to the source line by line (Figure 2). A bounded counterexample is a trace, and in our experience an interprocedural trace spanning several tens of methods is hard to act on unless a concrete test can be generated from it. Proof is incomplete under internal non-determinism. The witness is installed as a precondition, so the obligation is that every execution it admits violates the specification. A bug that manifests on some choice of internal non-determinism — a hash order, a clock, a service reply — cannot be discharged. Approaches based on Incorrectness logic [53] can alleviate this issue and also avoid unrolling loops with underapproximate loop summaries. Bounded search failures can be spurious. For bounded verifiers, it is difficult to distinguish true violations from the ones admitted due to the environment EF being under-constrained. On the other hand, a proof of refutation (whenever present) is a guarantee of a bug under the stated environment assumptions.

Evaluation

4.1

Setup

In this section we evaluate the efficacy of the NFV pipeline on our dataset. Unless stated otherwise the front end is gpt-5.6-sol, OpenAI’s flagship model at the time of writing, and the target is Dafny. Two budget parameters govern the proof search: an attempt discards the current translation and restarts from stage 1, while a repair round attempts to repair the proof failure through stage 4 only. All results use 5 attempts and 10 repair rounds, unless otherwise stated. We measure precision as the number of correct verdicts over verdicts issued, and recall as the number of correct verdicts issued over the entries of that class. Abstention is not counted as a verdict. F1 is their harmonic mean, which we report because the two are traded against each other: abstaining more raises precision and lowers recall.

4.2

The proof-based arm: Dafny

Table 3 gives the result on each task using the Dafny verifier backend. Of the 206 (program, specification) pairs, comprising the correct references and the incorrect mutants, the verification arm (row marked “verification”) generates a correctness proof in Dafny for 72 of the 103 correct reference implementations and issues proofs for 5 of the mutants labeled incorrect. This corresponds to a ≈70% recall and ≈93.5% precision. On the other hand, the refutation workflow (row marked “refutation”) produces a proof of violation for 47 of the 103 mutants while proving 6 reference 10

Table 4: The two tasks by library tier, one run each. verification

refutation

Tier

proved

bad

prec

refuted

bad

prec

L0 L1 L2a L2b L3

14/21 (67%) 18/22 (82%) 15/25 (60%) 22/26 (85%) 3/9 (33%)

0 2 1 0 2

100% 90% 94% 100% 60%

10/21 (48%) 11/22 (50%) 12/25 (48%) 13/26 (50%) 1/9 (11%)

1 0 2 1 2

91% 100% 86% 93% 33%

All

72/103 (70%)

94%

47/103 (46%)

89%

implementations incorrect on some input. This corresponds to a ≈46% recall and ≈89% precision. In addition, we create another configuration (“pipeline”) where we first run the refutation, and then run verification if refutation does not produce a proof. The combined pipeline produces a proof (of refutation or of verification) for 128 of the 206 tasks, marking a recall of 57.3% (118) and precision of 92.2% (118 / 128), and with an overall F1 score of 0.71. Table 4 breaks the same run down by library tier. A few points worth noting: • NFV struggles most with examples in the L3 tier for both the verification and refutation tasks, both in terms of precision and recall. The two have different causes. Recall is low because the imported libraries are hard to model, so the proof search more often gives up. The wrong verdicts are not caused by that modeling: Section 4.2.1 traces all four to preconditions the docstring never stated and to the argument types the translation chose. • On the other hand, NFV does well in both L0 and L2b tiers, each with a single incorrect claim. L0 benefits from the reduced need to model libraries; L2b benefits from the fact that higher-order functions such as filter can be easily mapped to Dafny’s comprehension support. • Finally, the lower performance on the L2a tier stems from the need to model strings in Dafny. This includes precisely modeling splitting and joining (.split, .join, .lstrip), case mapping (.lower, .upper, .swapcase) and character classification (.isalpha, .isnumeric); the stringhandling programs in that tier prove at 3/9. 4.2.1

Analysis

Eleven claims contradict a ground-truth label: 5 proofs of buggy programs and 6 counterexamples against correct ones. We investigated each of these and Table 5 attributes each to a cause. 4.2.2

Incorrect refutations

We assume that every reference implementation is correct with respect to the intent of its docstring, as we did when constructing the dataset in Section 2. A counterexample against a reference therefore leaves two possibilities: either the specification does not soundly formalize the docstring, or NFV mismodels the source code or its environment. Distinguishing the two can be subjective, because the intent of some docstrings is ambiguous. For example, the docstring for entry 49 (modp) documents “Return 2n modulo p (be aware of numerics)”, which does not say whether p must be positive or n non-negative. We are conservative: we blame NFV whenever there is any interpretation of the docstring under which the specification is sound. We arrive at the following conclusion: all 6 of them are real Python counterexamples to the postcondition as written, on inputs the docstring never excluded. For each, we name the missing precondition and explain briefly how it blocks the buggy input.

Table 5: Every wrong verdict of the reported run, by cause. entry is the kind of program the claim was made about: a reference is labeled correct and was refuted, a mutant is labeled incorrect and was proved. unstated assumption is the precondition the specification would have needed for the verdict and the label to agree. Every row is executed rather than asserted. task

entry

cause

unstated assumption

HumanEval 11 HumanEval 20 HumanEval 49 HumanEval 64 HumanEval 79 HumanEval 111 HumanEval 116 HumanEval 6 HumanEval 133 HumanEval 151 HumanEval 35

reference reference reference reference reference reference mutant mutant mutant mutant mutant

missing precondition missing precondition missing precondition missing precondition missing precondition missing precondition missing precondition stronger precondition stronger precondition stronger precondition library formalization

|a| = |b| no NaN p>0 ascii decimal ≥ 0 tokens are single letters arr[i] ≥ 0 no empty space-delimited field lst is integer-typed lst is integer-typed —

• 11 (string xor): |a| = |b|. The postcondition asserts |rv | = |a| = |b|, so on operands of unequal length it is unsatisfiable by any implementation. • 20 (find closest elements): No NaN. The witness is a pair of equal elements with ¬(x ≤ x) — admitted because PyFloat is abstract, and realizable because every comparison with NaN is false. • 49 (modp): p > 0. The witness is a negative modulus (n = 0, p = −1), which the theory’s requires b != 0 admits and Python computes without complaint. • 64 (vowels count): Only ascii argument. The specification counts vowels in s.lower() while the program tests the un-lowercased character, and "\u0130".lower() injects an i the program never sees. • 79 (decimal to binary): decimal ≥ 0. bin(-3)[2:] is ’b11’, which fails the ^db[01]+db$ match it is scored against. • 111 (histogram): tokens are single letters. The docstring “Given a string representing a space separated lowercase letters” seems to imply that a violating input such as "a aa" should not be considered. 4.2.3

Incorrect verifications

Spurious proofs come from a stronger precondition. a program more constrained than the Python one.

3 of the 5 are valid theorems about

• 6 (parse nested parens) has a stronger precondition. The docstring, in full, is “Input to this function is a string represented multiple groups for nested parentheses separated by spaces....” The inferred precondition includes a clause — the string is nonempty, and no space is leading, trailing or doubled — that rules out the buggy inputs ’’, ’() ’, ’ ()’ and ’() ()’ on which the mutant fails. • 133 (sum squares) and 151 (double the difference): a stronger precondition manifested as an incorrect type signature: the parameter lst in Python is translated as seq<int> in Dafny, which rejects the floating-point input on which the mutant fails. Incorrect library formalism: 35 (max element) computes the maximum of a list, and the specification asserts return value == max(l), where max is the Python built-in. The mutant 12

Table 6: Comparison of different LLMs for the proof-based tasks. proved is over the 103 correct programs, refuted over the 103 buggy ones, bad counts claims contradicting the label, prec is precision over claims, and F1 combines that precision with recall over the 103, counting an abstention as a wrong answer would count. type and audit split the entries that never reached the proof step: code that failed the type checker, and code that resolved but failed the artifact checks. Rows are ordered by decreasing verification F1. A row marked † was stopped before finishing: its refutation half is scored over the 203 entries that completed, not 206. The 3 that did not finish are the ones the model spent longest on. verification

gpt-5.6-sol gpt-5-mini claude-sonnet-4.6† claude-haiku-4.5

refutation

no proof attempted

proved

bad

prec

refuted

bad

prec

type

audit

72/103 (70%) 56/103 (54%) 41/103 (40%) 11/103 (11%)

5 38 12 2

94% 60% 77% 85%

0.80 0.57 0.53 0.19

47/103 (46%) 34/103 (33%) 39/101 (39%) 7/103 (7%)

6 17 2 0

89% 67% 95% 100%

0.60 0.44 0.55 0.13

1 72 0 92

9 20 159 257

adds 1 to the return value, violating that specification. The translated obligation is result == PyMax(l), and PyMax is a function stage 1 wrote by transcribing the mutant’s own loop, its base case adding 1 to the result and so introducing the same bug into the specification. Incorrect label: Finally, 116 (sort array) is an entry where NFV changes the label of the mutant. The docstring for this example says “an array of non-negative integers” and the mutant fails the specification only for negative values. NFV installs a correct precondition and is therefore able to prove that the mutant satisfies the postcondition. The problem came not from the nl2postcond dataset, but from the EvalPlus dataset, which added a test case containing a negative integer that violates the precondition.

4.3

The bounded-verifier arm: CBMC

In this section, we discuss instantiating NFV with CBMC, a bounded program verifier, taking C as the formal language. Because CBMC does not support rich specification constructs, the agent writes C code for the libraries from their documentation. Given the bounded nature of the verification, we only focus on the effectiveness of this arm for refutation. Besides compiling without errors, the translated C program must be free of undefined behavior (UB), which CBMC’s built-in UB checks establish: overflow, bounds, pointer and conversion checks. CBMC issues 72 counterexamples, of which 65 refute a mutant program and 7 are false: that is a recall of 63% over the 103 buggy programs at 90% precision, against the Dafny arm’s 46% at 89% on the same programs. This offers an alternative for refutation when bounded verification can scale. The precondition is again the dominant source of unsound refutations, the same diagnosis Section 4.2.1 reaches for the proof arm using Dafny.

4.4

Weaker LLMs

Both arms were re-run with three further LLMs in place of gpt-5.6-sol, holding prompts, checks, backend and budget fixed. We observe that: • gpt-5.6-sol is the only model that can provide value for this dataset with around 90% precision and around 58% recall. • claude-haiku-4.5 performs quite poorly on both tasks. It also has the largest number of examples where the translated Dafny code failed to type check or pass the audits. 13

• Degradation is task-asymmetric, and refutation is the resilient direction. • There is a sharp drop in the verification capability of weaker models compared to gpt-5.6-sol due to either reduced recall (claude-sonnet-4.6) or reduced precision (gpt-5-mini) or both. Both of these models have substantially more typechecking and audit failures.

4.5

Strawman and symbolic baselines

We compare NFV against three baselines spanning a spectrum from fully neural to fully symbolic. LLM-as-a-judge. The LLM is shown the program and the specification in Python — with the docstring’s input assumptions supplied — and asked whether one satisfies the other. It commits on every one of the 206 entries, never abstaining, and refutes 76% of a corpus that is half correct. Overall, it is wrong on 58 of the 206 entries at 72% precision (compared to the 92% precision NFV provides through its ability to abstain when it cannot back its verdict with a proof artifact): it rejects 56 of the 103 correct programs and accepts 2 of the 103 incorrect ones. The failure is not only the error rate but what is left behind: an opinion, with no artifact anyone can check and no witness anyone can run. LLM+verifier. The second baseline asks for a verifiable Dafny method carrying the specification, with a repair loop against the verifier and nothing else — one call, no separated stages, nothing written blind, no freeze and no checks. It proves 98% of the correct programs and 98% of the known-wrong ones: precision 50%. However, the program and specification being proved are not the intended ones, since the agent is incentivized merely to find a proof: the code is rewritten (57% of unsound proofs), the library invented (35%), the precondition strengthened until the bug falls outside it (56%). A proof is only as good as the artifact it is about, so the discipline that fixes the artifact, not the proof search, is what NFV provides. A sound verifier. We also explored Nagini, a symbolic Python verifier [42] that leverages SMT solvers for proofs. Given a type-annotated program with contracts, it discharges obligations comparable to the ones Dafny discharges here. In its default configuration it proves 0% on this corpus, because 83% of the entries are rejected for want of type-annotated signatures, which these programs do not carry. Asking an agent to supply good guesses at these annotations raises the fraction that reach the verifier to 98%, but raises the proof rate only to 2%. This result is not a judgment of the capability of Nagini on this dataset, but rather a demonstration of the utility of NFV. We attribute the low success rate to the absence of a formal environment specification EF (including preconditions that are vital even for tier L0 without any libraries) that symbolic verifiers assume, and to the absence of proof automation — precisely the burden that symbolic verification tools place on their end users.

Related work

Neuro-formal verification is inspired by decades-long investment in symbolic program verifiers and recent progress in AI agents. We describe a few (far from exhaustive) prior works in these two domains.

5.1

Symbolic program verification

Translation-based verifiers: Verifying a program by translating it into an (intermediate) verification language is long-standing practice. Spec# [17] translates an annotated dialect of C#, VCC [14] and Havoc [19] translate C, VeriSol [26] translates Solidity, and Dafny [43] compiles its own source language, all of them into Boogie [16] and from there into SMT. CSLib [18] is 14

developing Lean libraries for the semantics of languages and program logics, which will make these translations more trusted and reusable. Extended-static checkers: NFV is inspired by works on extended static checking [31]: the verification is performed on a formal model of the source code, even though the formalism may be optimistic or “soundy” [30]. Such a translation either targets a fragment of the language or adopts optimistic assumptions that trade soundness for coverage of the code it can analyze. Tools (such as SDV, HAVOC, etc.) of this genre have been deployed on production software for “proofs” of properties in systems code [32, 38, 39, 52], where the value delivered is hard-to-find defects an engineer confirms and fixes. Environment modeling: All of these formal verification efforts work on closed programs and face the problem of modeling the environment of an open program, which leaves end-to-end soundness either in the hands of the user [27] or in heuristic inference of environment assumptions like angelic verification [28, 29]. We envision NFV helping to unlock the value of formal verification to mainstream developers without being constrained to specific languages and domains by leveraging progress in AI agents along three directions discussed below.

5.2

Agentic program reasoning

Neural language translation — predates the current generation of agents/models [20, 21, 22] but has advanced quickly with them [23, 25]. NFV will benefit from defining datasets for translating from mainstream languages into verification-aware languages, where we ensure equivalence through tests or symbolic means. Intent formalization — the process of generating and validating formal program specifications from informal documentation such as docstrings [47], a concept related to autoformalization [24] from formal mathematics. These specifications can be attested through symbolic validation against a program’s tests [48] without the need for implementations, to ensure their soundness, completeness and precision (modulo tests). Such techniques were previously manual, but have benefited from agentic proof automation [49]. This will alleviate the need for end-users of NFV to inspect nontrivial library specifications at the cost of inspecting concrete tests in the source language that are much more familiar to them. Agentic proof automation — progress has been rapid in invariant synthesis with language models [51, 50], whole-proof generation and repair [41], retrieval-augmented tactic prediction [33], and proof generation for Verus [34] and Dafny [40]. We foresee continuous benefit from improvements in frontier model capability.

Conclusion and Future Work

We presented neuro-formal verification as a simple integration of AI coding agents and verificationaware languages to facilitate language-agnostic formal program reasoning. We have demonstrated that recent progress enables this capability: the pipeline issues a machine-checked verdict on 57% of a dataset at 92% precision. The dataset remains challenging for the current flagship model, which leaves the remaining 43% without a proof. Much research needs to be done to bring this to mainstream software developers not versed in formal verification. We need to curate labeled datasets that are increasingly representative of real-world software development tasks covering richer libraries and concurrency. Increasing the trustworthiness of each agentic component through symbolic techniques will be helpful. For example, a benchmark of code translation into verification-aware languages, evaluated through 15

tests or other symbolic means, can help make this component robust. Similarly, we need real-world benchmarks for intent formalization, and techniques to evaluate the quality of agent-generated specifications for the environment against existing artifacts such as tests [47, 48]. Finally, the advances should be grounded by realistic user studies to understand the utility of the approach including the evaluation of informal concepts such as proof sketches. Posing formal program reasoning as an empirical accuracy problem — rather than a Boolean question of soundness — makes it measurable: it can be compared across models and improved by the methods that improve any other learned component. This may be a new and more holistic way of thinking for researchers and practitioners building formal reasoning tools for mainstream developers.

References [1] A. M. Turing. Checking a Large Routine. In Report of a Conference on High Speed Automatic Calculating Machines, Cambridge, 1949. [2] C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 1969. [3] L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language. In CADE, 2021. [4] E. Ioannidis, N. Swamy, G. Ebner, M. Philipose and T. Ramananandro. Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report). Proc. ACM Program. Lang. 10(ICFP), Article 311, 2026. [5] C. Barrett, P. Fontaine and C. Tinelli. The SMT-LIB Standard: Version 2.6. Department of Computer Science, The University of Iowa, https://smt-lib.org, 2016. [6] L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS, 2008. [7] The Rocq Development Team. The Rocq Prover (formerly Coq). Inria, https://rocq-prover. org, 2025. [8] T. Nipkow, L. C. Paulson and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer LNCS 2283, 2002. [9] N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss et al. Dependent Types and Multi-Monadic Effects in F⋆ . In POPL, 2016. [10] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish et al. seL4: Formal Verification of an OS Kernel. In SOSP, 2009. [11] X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7), 2009. [12] K. Bhargavan, B. Bond, A. Delignat-Lavaud, C. Fournet, C. Hawblitzel, C. Hriţcu, S. Ishtiaq, M. Kohlweiss, R. Leino, J. Lorch et al. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In SNAPL, 2017. 16

[13] J. W. Cutler, C. Disselkoen, A. Eline, S. He, K. Headley, M. Hicks, K. Hietala, E. Ioannidis, J. Kastner, A. Mamat et al. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. In OOPSLA, 2024. [14] E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte and S. Tobies. VCC: A Practical System for Verifying Concurrent C. In TPHOLs, 2009. [15] A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y. Zhou, J. Howell, B. Parno and C. Hawblitzel. Verus: Verifying Rust Programs Using Linear Ghost Types. In OOPSLA, 2023. [16] M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs and K. R. M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO, LNCS 4111, 2006. [17] M. Barnett, K. R. M. Leino and W. Schulte. The Spec# Programming System: An Overview. In CASSIS, LNCS 3362, 2005. [18] C. W. Barrett, S. Chaudhuri, F. Montesi, J. Grundy, P. Kohli, L. de Moura, A. Rademaker and S. Yingchareonthawornchai. CSLib: The Lean Computer Science Library. CoRR, abs/2602.04846, 2026. [19] S. K. Lahiri and S. Qadeer. Back to the Future: Revisiting Precise Program Verification using SMT Solvers. In POPL, 2008. [20] B. Roziere, M.-A. Lachaux, L. Chanussot and G. Lample. Unsupervised Translation of Programming Languages. In NeurIPS, 2020. [21] B. Rozière, J. M. Zhang, F. Charton, M. Harman, G. Synnaeve and G. Lample. Leveraging Automated Unit Tests for Unsupervised Code Translation. In ICLR, 2022. [22] M. Szafraniec, B. Rozière, H. Leather, P. Labatut, F. Charton and G. Synnaeve. Code Translation with Compiler Representations. In ICLR, 2023. [23] Z. Yang, F. Liu, Z. Yu, J. W. Keung, J. Li, S. Liu, Y. Hong, X. Ma, Z. Jin and G. Li. Exploring and Unleashing the Power of Large Language Models in Automated Code Translation. Proc. ACM Softw. Eng., 1(FSE), 2024. [24] Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik and C. Szegedy. Autoformalization with Large Language Models. In NeurIPS, 2022. [25] R. Pan, A. R. Ibrahimzada, R. Krishna, D. Sankar, L. P. Wassi, M. Merler, B. Sobolev, R. Pavuluri, S. Sinha and R. Jabbarvand. Lost in Translation: A Study of Bugs Introduced by Large Language Models while Translating Code. In ICSE, 2024. [26] Y. Wang, S. K. Lahiri, S. Chen, R. Pan, I. Dillig, C. Born, I. Naseer and K. Ferles. Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. In VSTTE, LNCS 12031, 2020. [27] S. Priya, T. Kahsai and A. Gurfinkel. Unlocking the Power of Environment Assumptions for Unit Proofs. In SEFM, LNCS 15280, 2024. [28] A. Das, S. K. Lahiri, A. Lal and Y. Li. Angelic Verification: Precise Verification Modulo Unknowns. In CAV, LNCS 9206, 2015.

[29] S. K. Lahiri, A. Lal, S. Gopinath, A. Nutz, V. Levin, R. Kumar, N. Deisinger, J. Lichtenberg and C. Bansal. Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. In FMCAD, 2020. [30] B. Livshits, M. Sridharan, Y. Smaragdakis, O. Lhoták, J. N. Amaral, B.-Y. E. Chang, S. Z. Guyer, U. P. Khedker, A. Møller and D. Vardoulakis. In Defense of Soundiness: A Manifesto. Communications of the ACM, 58(2):44–46, 2015. [31] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata. Extended Static Checking for Java. In PLDI, 2002. [32] J. Vanegue and S. K. Lahiri. Towards Practical Reactive Security Audit Using Extended Static Checkers. In IEEE Symposium on Security and Privacy, 2013. [33] K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger and A. Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In NeurIPS Datasets and Benchmarks, 2023. [34] C. Yang, X. Li, M. R. H. Misu, J. Yao, W. Cui, Y. Gong, C. Hawblitzel, S. K. Lahiri, J. R. Lorch, S. Lu, F. Yang, Z. Zhou and S. Lu. AutoVerus: Automated Proof Generation for Rust Code. In OOPSLA, 2025. [35] A. Karpathy. Vibe coding. Post on X, February 2025. [36] F. Kirchner, N. Kosmatov, V. Prévosto, J. Signoles and B. Yakobowski. Frama-C: A Software Analysis Perspective. Formal Aspects of Computing, 27(3):573–609, 2015. [37] E. Clarke, D. Kroening and F. Lerda. A Tool for Checking ANSI-C Programs. In TACAS, 2004. [38] T. Ball, B. Hackett, S. K. Lahiri, S. Qadeer and J. Vanegue. Towards Scalable Modular Checking of User-Defined Properties. In VSTTE, LNCS 6217, 2010. [39] T. Ball, V. Levin and S. K. Rajamani. A Decade of Software Model Checking with SLAM. Communications of the ACM, 54(7):68–76, 2011. [40] M. R. H. Misu, C. V. Lopes, I. Ma and J. Noble. Towards AI-Assisted Synthesis of Verified Dafny Methods. In FSE, 2024. [41] E. First, M. N. Rabe, T. Ringer and Y. Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. In FSE, 2023. [42] M. Eilers and P. Müller. Nagini: A Static Verifier for Python. In CAV, 2018. [43] K. R. M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR, 2010. [44] M. Chen, J. Tworek, H. Jun, Q. Yuan, H. Pondé de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman et al. Evaluating Large Language Models Trained on Code. arXiv:2107.03374, 2021. [45] J. Liu, C. S. Xia, Y. Wang and L. Zhang. Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code. In Advances in Neural Information Processing Systems (NeurIPS), 2023. 18

[46] M. Endres, S. Fakhoury, S. Chakraborty and S. K. Lahiri. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? In FSE, 2024. [47] S. K. Lahiri. Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents. arXiv:2603.17150, 2026. [48] S. K. Lahiri. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. In FMCAD, 2024. [49] N. Swamy and S. K. Lahiri. Spotting Specification Gaps with Small Proof-Oriented Tests. RiSE MSR Blog, Microsoft Research, April 2026. https://risemsr.github.io/blog/ 2026-04-16-spotting-specs/. [50] H. Wu, C. Barrett and N. Narodytska. Lemur: Integrating Large Language Models in Automated Program Verification. In ICLR, 2024. [51] A. Kamath, A. Senthilnathan, S. Chakraborty, P. Deligiannis, S. K. Lahiri, A. Lal, A. Rastogi, S. Roy and R. Sharma. Finding Inductive Loop Invariants using Large Language Models. In FMCAD, 2024. [52] A. Lal, S. Qadeer, and S. K. Lahiri. A Solver for Reachability Modulo Theories. In CAV, 2012. [53] P. W. O’Hearn. Incorrectness Logic. Proceedings of the ACM on Programming Languages, 4(POPL), 2020.

Dataset details

A.1

The benchmark in full

Table 7 lists every task in nl2post-safe with the postcondition its two entries are scored against, together with the upstream identifiers that pin the pair. Table 7: The 103 pairs — all 206 entries — with the postcondition each pair is scored against, and the upstream identifiers that pin it. task is the HumanEval number. p is the response num selecting the postcondition in summary eval results.jsonl and raw preprocessed samples.jsonl. m is the response num selecting the mutant in distinct code mutants.jsonl; below 200 it is a natural mutant, at 200 and above an artificial one. The reference and the mutant of a task share a postcondition, so one row covers two entries. Postconditions are reproduced after sanitization (Appendix A), which is the form the pipeline sees. task

entry point

postcondition

separate paren groups

2 3

truncate number below zero

0 0

202 200

4 5

mean absolute deviation intersperse

1 0

213 27

parse nested parens

sum product

assert all((s.count(’(’) == s.count(’)’) and ’()’ in s for s in return value)) assert 0 <= return value < 1 assert return value == True and any((sum( operations[:i + 1]) < 0 for i in range(len( operations)))) or return value == False assert 0 <= return value assert len(return value) == len(numbers) * 2 - 1 if numbers else len(return value) == 0 assert len(return value) == len(paren string.split() ) assert sum(numbers) == return value[0]

task

entry point

postcondition

rolling max

106

make palindrome

string xor

greatest common divisor

205

parse music

202

sort numbers

find closest elements

147

21 25 26 30 31 33

rescale to unit factorize remove duplicates get positive is prime sort third

1 1 0 0 0 0

200 202 205 200 27 5

34 35 36

unique max element fizz buzz

0 0 0

200 201 205

37 41

sort even car race collision

5 0

11 7

incr list

200

pairs sum to zero

44 45 47

change base triangle area median

0 0 4

60 200 200

49 50 51

modp decode shift remove vowels

1 9 0

1 289 200

53 56

add correct bracketing

0 0

200 200

58 59 60 61

common largest prime factor sum to n correct bracketing

0 1 0 0

203 44 189 201

vowels count

assert all((return value[i] >= max(numbers[:i + 1]) for i in range(len(numbers)))) assert return value.startswith(string) and return value == return value[::-1] assert len(return value) == len(a) == len(b) and all((ch in ’01’ for ch in return value)) assert a % return value == 0 and b % return value == 0 assert len(return value) == len([note for note in music string.split() if note in [’o’, ’o|’, ’.|’]]) assert return value == ’ ’.join(sorted(numbers. split(), key=lambda x: [’zero’, ’one’, ’two’, ’ three’, ’four’, ’five’, ’six’, ’seven’, ’eight’, ’ nine’].index(x))) assert return value in [(x, y) for i, x in enumerate(numbers) for j, y in enumerate(numbers) if i != j and x <= y] assert len(numbers) == len(return value) assert n == eval(’*’.join(map(str, return value))) assert len(return value) == len(set(return value)) assert all((i > 0 for i in return value)) assert n < 2 and (not return value) or n >= 2 assert all((l[i] == return value[i] for i in range( len(l)) if i % 3 != 0)) assert return value == sorted(list(set(l))) assert return value == max(l) assert isinstance(return value, int) and return value >= 0 assert sorted(return value[::2]) == sorted(l[::2]) assert isinstance(return value, int) and return value >= 0 assert all((return value[i] == l[i] + 1 for i in range(len(l)))) assert not return value or any((x + y == 0 for i, x in enumerate(l) for j, y in enumerate(l) if i != j) ) assert int(return value, base) == x assert return value == 0.5 * a * h assert sum((i <= return value for i in l)) >= len( l) // 2 and sum((i >= return value for i in l)) >= len(l) // 2 assert 0 <= return value < p assert len(s) == len(return value) assert all((c not in ’aeiouAEIOU’ for c in return value)) assert return value == x + y assert return value == False or brackets.count(’<’) == brackets.count(’>’) assert return value == sorted(return value) assert n % return value == 0 assert return value == n * (n + 1) // 2 assert return value == False or brackets.count(’(’) == brackets.count(’)’) assert return value == s.lower().count(’a’) + s. lower().count(’e’) + s.lower().count(’i’) + s. lower().count(’o’) + s.lower().count(’u’) + (1 if s.lower().endswith(’y’) else 0)

task

entry point

postcondition

65 66

circular shift digitSum

0 6

7 200

fruit distribution

pluck

70 71

strange sort list triangle area

0 0

48 210

73 77

smallest change iscube

2 2

0 0

hex key

203

decimal to binary

81 86 87

numerical letter grade anti shuffle get row

0 2 0

215 0 3

88 89 90

sort array encrypt next smallest

0 0 3

206 3 6

93 96

encode count up to

1 3

17 1

97 99

multiply closest integer

0 9

100

make a pile

102

choose num

103

rounded avg

104

unique digits

126

105

by length

203

106

assert len(str(x)) == len(return value) assert sum((ord(char) for char in s if char. isupper())) == return value import re assert isinstance(return value, int) and return value >= 0 and (return value == n - sum(map( int, re.findall(’\\d+’, s)))) assert isinstance(return value, list) and (len( return value) == 2 and return value[0] % 2 == 0 and (arr[return value[1]] == return value[0])) or (return value == [] and all((i % 2 != 0 for i in arr))) assert return value == max([num for num in set(lst) if lst.count(num) >= num], default=-1) assert len(lst) == len(return value) assert isinstance(return value, float) and round( return value, 2) == return value or return value == -1 assert 0 <= return value <= len(arr) // 2 assert return value == (round(abs(a) ** (1.0 / 3)) ** 3 == abs(a)) assert isinstance(return value, int) and 0 <= return value <= len(num) import re assert re.match(’^db[01]+db$’, return value) assert len(grades) == len(return value) assert len(s) == len(return value) assert all((return value[i][0] < return value[i + 1] [0] or (return value[i][0] == return value[i + 1][0] and return value[i][1] >= return value[i + 1][1]) for i in range(len(return value) - 1))) assert len(array) == len(return value) assert len(s) == len(return value) assert (return value is None) == (len(set(lst)) < 2) assert len(return value) == len(message) assert all((i < n and all((i % j != 0 for j in range(2, int(i ** 0.5) + 1))) for i in return value)) assert return value == abs(a) % 10 * (abs(b) % 10) assert isinstance(return value, int) and abs( return value - float(value)) <= 1 assert len(return value) == n and all((return value[ i] == return value[i - 1] + 2 for i in range(1, n)) ) assert return value == -1 or (x <= return value <= y and return value % 2 == 0 and all((i <= return value for i in range(x, y + 1) if i % 2 == 0))) assert isinstance(return value, str) and return value.startswith(’0b’) and all((c in ’01’ for c in return value[2:])) or return value == -1 assert all((str(i)[j] in ’13579’ for i in return value for j in range(len(str(i))))) and return value == sorted(return value) assert all((item in [’One’, ’Two’, ’Three’, ’Four’, ’Five’, ’Six’, ’Seven’, ’Eight’, ’Nine’] for item in return value)) and len(return value) <= len(arr) assert len(return value) == n

task

entry point

postcondition

107

even odd palindrome

140

108

count nums

110

exchange

111

histogram

112

reverse delete

205

113 114

odd count minSubArraySum

0 4

220 0

115

max fill

116

sort array

117

select words

118

get closest vowel

120

maximum

121

solution

123

get odd collatz

127 128

intersection prod signs

0 2

235 77

130 131

tri digits

0 0

3 18

133

sum squares

151

135

can arrange

136

largest smallest integers

115

141

file name check

assert sum(return value) == len([i for i in range( 1, n + 1) if str(i) == str(i)[::-1]]) assert isinstance(return value, int) and 0 <= return value <= len(arr) assert (return value == ’YES’) == (len([num for num in lst1 if num % 2 != 0]) <= len([num for num in lst2 if num % 2 == 0])) assert all([isinstance(key, str) and key.islower( ) and isinstance(value, int) and (value == test. count(key)) for key, value in return value.items()] ) assert return value[1] == (return value[0] == return value[0][::-1]) assert len(lst) == len(return value) assert return value == min((sum(nums[i:j]) for i in range(len(nums)) for j in range(i + 1, len(nums) + 1))) assert isinstance(return value, int) and return value >= 0 assert all((bin(return value[i]).count(’1’) <= bin(return value[i + 1]).count(’1’) and (bin( return value[i]).count(’1’) != bin(return value[i + 1]).count(’1’) or return value[i] <= return value[ i + 1]) for i in range(len(return value) - 1))) assert all((sum((1 for c in word if c.lower() not in ’aeiou ’)) == n for word in return value)) and all((word in return value for word in s.split() if sum((1 for c in word if c.lower() not in ’aeiou ’)) == n)) assert return value == ’’ or return value in ’ AEIOUaeiou’ assert len(return value) == k and all((return value[ i] <= return value[i + 1] for i in range(len( return value) - 1))) assert isinstance(return value, int) and return value == sum((x for i, x in enumerate(lst) if i % 2 == 0 and x % 2 == 1)) assert return value == sorted(return value) and all( (num % 2 != 0 for num in return value)) assert return value in [’YES’, ’NO’] assert isinstance(return value, int) and len(arr) > 0 or (return value is None and len(arr) == 0) assert len(return value) == n + 1 assert return value == 0 if all((int(digit) % 2 == 0 for digit in str(n))) else True assert isinstance(return value, int) and return value >= 0 assert return value == -1 and sorted(arr) == arr or (return value > 0 and arr[return value] < arr[ return value - 1]) assert return value[0] == max(filter(lambda x: x < 0, lst), default=None) and return value[1] == min( filter(lambda x: x > 0, lst), default=None) assert return value == ’Yes’ and (file name[0]. isalpha() and file name.split(’.’)[1] in [’txt’, ’ exe’, ’dll’]) or return value == ’No’

task

entry point

postcondition

143

words in sentence

200

145 146

order by points specialFilter

3 0

134 49

148

205

150 151

x or y double the difference

0 1

113 4

152 153

compare Strongest Extension

1 1

206 4

155 156

even odd count int to mini roman

0 1

8 203

157

right angle triangle

159

eat

161

solve

163

generate integers

128

assert all((word in sentence.split() and len(word) in [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97] for word in return value.split())) assert len(nums) == len(return value) assert return value == len([num for num in nums if num > 10 and int(str(num)[0]) % 2 != 0 and (int( str(num)[-1]) % 2 != 0)]) assert isinstance(return value, tuple) and all(( isinstance(planet, str) for planet in return value) ) assert return value in {x, y} assert isinstance(return value, int) and return value >= 0 assert len(return value) == len(game) == len(guess) assert return value == class name + ’.’ + max( extensions, key=lambda x: sum((1 for c in x if c. isupper())) - sum((1 for c in x if c.islower()))) assert sum(return value) == len(str(abs(num))) assert isinstance(return value, str) and all((char in ’ivxlcdm’ for char in return value)) assert return value == True and (a ** 2 + b ** 2 == c ** 2 or a ** 2 + c ** 2 == b ** 2 or b ** 2 + c * * 2 == a ** 2) or (return value == False and (not ( a ** 2 + b ** 2 == c ** 2 or a ** 2 + c ** 2 == b * * 2 or b ** 2 + c ** 2 == a ** 2))) assert return value == [min(number + need, number + remaining), max(0, remaining - need)] assert all((ch.isalpha() and ch.swapcase() == s[i] or (not ch.isalpha() and (ch == s[i] or ch == s[-(i + 1)])) for i, ch in enumerate(return value))) assert all((i % 2 == 0 for i in return value))

An example program from each library tier

L0 — HumanEval/157. It uses nothing beyond arithmetic, indexing and control flow. Nothing outside the program has to be described, so the model’s trusted base can be empty. def r i g h t _angle_triangle (a , b , c ) : return a ** 2 + b ** 2 == c ** 2 or a ** 2 + c ** 2 == b ** 2 or b ** 2 + c ** 2 == a ** 2

L1 — HumanEval/121. Beyond arithmetic, indexing and control flow it uses sum. Each call here is one self-contained, total function whose meaning the model can state in a line. def solution ( lst ) : return sum (( lst [ i ] for i in range ( len ( lst ) ) if i % 2 == 0 and lst [ i ] % 2 == 1) )

L2a — HumanEval/120. Beyond arithmetic, indexing and control flow it uses .sort, sorted. A faithful specification has to relate whole collections — what the result contains, and in what order — rather than give a single value. 23

def maximum ( arr , k ) : return sorted ( sorted ( arr ) [:: -1][: k ])

L2b — HumanEval/30. Beyond arithmetic, indexing and control flow it uses filter, list. The specification must quantify over an argument whose body it cannot see, which is a different demand from describing a collection. def get_positive ( l : list ) : return list ( filter ( lambda x : x > 0 , l ) )

L3 — HumanEval/133. Beyond arithmetic, indexing and control flow it uses import math, map, math.ceil, sum. The boundary is not the model’s to choose: it must axiomatise a surface defined elsewhere, and any axiom it writes about that surface is assumed, not checked. def sum_squares ( lst ) : import math return sum ( map ( lambda x : math . ceil ( x ) ** 2 , lst ) )

Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning

Analyze & explore related research in Conceptio

Related documents