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

A paper submitted to arXiv on 21 Aug 2026 and revised 14 Sep 2026 introduces neuro-formal verification (NFV), a method in which an AI coding agent formalizes source-level verification problems into proof obligations in a verification-aware language discharged by an established sound verifier. In experiments on a balanced dataset of correct and buggy Python solutions, NFV with a Dafny backend correctly resolved 57% of all entries at 92% precision, while a CBMC backend produced a counterexample for 63% of buggy programs at 90% precision. The authors report that an LLM-as-judge baseline reached only 72% precision with no checkable artifact, and an unstaged agent-verifier combination proved 98% of both correct and known-buggy programs at 50% precision.

Computer Science Software Engineering Submitted on 21 Aug 2026 v1 https://arxiv.org/abs/2608.21516v1 , last revised 14 Sep 2026 this version, v3 Title:Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning View PDF https://arxiv.org/pdf/2608.21516 HTML experimental https://arxiv.org/html/2608.21516v3 Abstract:Formal verification provides the strongest correctness guarantees for software, and verification-aware languages can produce sound, machine-checked proofs. Recent AI coding agents have sharply lowered the cost of constructing such proofs. Yet few mainstream developers benefit: most use languages without formal-verification support, and formalizing properties and modeling execution environments demand formal-methods expertise. Proof therefore remains reserved for a few notable artifacts, while production software is attested mainly through review and testing. We introduce neuro-formal verification NFV , which brings this automation to mainstream languages. An AI coding agent formalizes a source-level verification problem into a proof obligation in a verification-aware language, discharged by an established sound verifier aided by agentic proof search. Staged, goal-blind transformations reduce the risk of proving an artifact that does not faithfully represent the source program, property, or environment. Since NFV cannot ensure the soundness of this formalization, it optimizes for empirical accuracy rather than end-to-end soundness, while insisting on machine-checked evidence for every verdict. Experiments with current frontier models on a balanced dataset of correct and buggy Python solutions demonstrate the effectiveness of our approach. NFV with Dafny correctly resolves 57% of all entries, at 92% precision among its verdicts; with a CBMC backend, it produces a counterexample for 63% of the buggy programs at 90% precision. In contrast, an LLM-as-judge baseline achieves only 72% precision while answering every entry without any checkable artifact, and an unstaged agent-verifier combination proves 98% of both the correct and the known-buggy programs, yielding only 50% precision. Together, they confirm that both proofs and staging benefit an AI agent's formal program reasoning. Submission history From: Shuvendu Lahiri view email https://arxiv.org/show-email/c549eca6/2608.21516 Fri, 21 Aug 2026 18:00:02 UTC 121 KB \ v1\ https://arxiv.org/abs/2608.21516v1 Wed, 26 Aug 2026 05:46:01 UTC 121 KB \ v2\ https://arxiv.org/abs/2608.21516v2 v3 Mon, 14 Sep 2026 09:08:25 UTC 123 KB References & Citations Loading... Bibliographic and Citation Tools Bibliographic Explorer What is the Explorer? https://info.arxiv.org/labs/showcase.html arxiv-bibliographic-explorer Connected Papers What is Connected Papers? https://www.connectedpapers.com/about Litmaps What is Litmaps? https://www.litmaps.co/ scite Smart Citations What are Smart Citations? https://www.scite.ai/ Code, Data and Media Associated with this Article alphaXiv What is alphaXiv? https://alphaxiv.org/ CatalyzeX Code Finder for Papers What is CatalyzeX? https://www.catalyzex.com DagsHub What is DagsHub? https://dagshub.com/ Gotit.pub What is GotitPub? http://gotit.pub/faq Hugging Face What is Huggingface? https://huggingface.co/huggingface ScienceCast What is ScienceCast? https://sciencecast.org/welcome Demos Recommenders and Search Tools Influence Flower What are Influence Flowers? https://influencemap.cmlab.dev/ CORE Recommender What is CORE? https://core.ac.uk/services/recommender arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs https://info.arxiv.org/labs/index.html .