Formal Methods in the Agentic AI Era: A Strategic Agenda for High-Assurance Software

tl;dr — LLMs are increasingly used for code generation, while researchers also warn that their outputs often look correct but miss functional requirements. That makes correctness, auditability, and policy compliance more — not less — valuable.

Complimentary Reading

Because AI makes code easy to produce and hard to trust, we need verification and provability.

Provability answers: "Is this system correct for the properties that matter?"
Verifiability answers: "Can others check that claim independently?"
In agentic coding, the main risk is plausible but wrong software. Proofs, tests, model checks, runtime monitors, and audit trails turn fast code generation into trustworthy engineering.

When code becomes cheap, assurance becomes valuable.

Modern verification now spans a broad spectrum, ranging from traditional theorem proving and model checking to cutting-edge cryptographic verifiable computation.

AI serves as both a powerful automation tool for generating proofs and a complex new target that requires specialized robustness and safety checks. High-stakes industries like aerospace, medicine, and finance are increasingly adopting layered assurance strategies to mitigate risks in software supply chains and autonomous systems.

Ultimately, achieving trustworthy software in the age of AI requires a combination of mathematically rigorous evidence, runtime monitoring, and transparent provenance frameworks.

The strongest evidence today is in targeted domains: seL4 for kernels, CompCert for high-assurance C compilation, Project Everest for verified cryptography and parsers, and AWS Automated Reasoning checks for constraining GenAI outputs against formal business rules. CompCert also reports a March contemporary qualification milestone for critical avionics software, which is a notable sign of industrial maturity.

At the same time, AI is reducing proof friction. DeepMind's AlphaProof and AlphaGeometry 2 reached silver-medal level at the 2024 IMO; Microsoft's AutoVerus reports correct proof generation on more than 90% of a 150-task benchmark, and VeruSAGE reports over 80% completion on an 849-task benchmark. DARPA's PROVERS program explicitly aims to turn this into a scalable engineering practice by reducing proof repair work and making formal methods more accessible to non-experts.

The caveat is maturity. A 2025 systematic mapping study says AI-for-formal-methods is still "yet to mature," heavily concentrated in theorem proving, and short on shared benchmarks and case studies. Berkeley researchers similarly argue that "correctness, not just plausibility" must become the governing principle for LLM-based code translation. The operating model, then, is hybrid assurance: use AI to draft code, specs, annotations, and proof steps, but keep formal specifications, compositional reasoning, and trusted proof checkers in the loop.

Provable and Verifiable Software in the Age of AI

Think about the software you rely on every single day — I am not talking about a streaming app crashing or your web browser freezing up.

Think about the code running the anti-lock brakes in your car when you slam on them at 70 miles per hour. Or think about the cryptographic algorithms locking down smart contracts holding a company's entire liquidity. Or even medical devices, like the firmware dictating the exact microdosage of insulin in a continuous glucose monitor.

So the question is, how do we actually know — without a shadow of a doubt — that those systems won't fail when lives or billions of dollars are on the line?

Because you can't just rely on a team of engineers running a few thousand unit tests before launch anymore. We are talking about the need for absolute mathematical certainty, which is a massive engineering hurdle.

Historically, the tech industry has leaned on testing to find bugs. You write the code, throw a bunch of edge-case scenarios at it, and if it passes, you ship it. It's the old "move fast and break things" mantra. But testing can only prove the presence of bugs; it can never prove their absence. For high-stakes environments, that paradigm is completely dead. You can no longer ask, "Does this code work in our test suite?" You now have to ask, "Can you produce machine-checkable, mathematically sound evidence that this code will always execute its intended specification, no matter the inputs?"

AI is now actively writing — and in many cases running — a staggering amount of this code. We've introduced a massive speed multiplier into the ecosystem, and speed is traditionally the enemy of thorough verification.

What's fascinating is the dual nature of AI in this landscape.

It is simultaneously the biggest threat to software assurance and the most promising tool for achieving it. It's a total paradox.

AI as the Target of Verification

Let's look at AI as the target of verification first. We are increasingly putting neural networks — like learned controllers for autonomous systems — right inside critical infrastructure.

Which is terrifying when you think about it. A traditional software program is just a series of logical branches; if A, then B. A human can read and trace it. But a neural network is just a black box of billions of weights, biases, and high-dimensional matrix multiplications. You cannot just read the code to see what it does. The "code" is essentially just math reacting to probabilities.

So how do you even prove a probability is safe?

You have to map out boundaries in that high-dimensional space. The focus completely shifts to proving two things: robustness and reachability.

Robustness asks a mathematical question. Say you take an input, like a stop sign seen by an autonomous vehicle's camera, and you perturb the pixels by an imperceptible fraction — noise a human wouldn't even notice. Does the output of the neural network drastically fail and classify it as a speed limit sign? If it does, it's not robust.

Reachability analysis, on the other hand, uses complex geometry to calculate the absolute limits of a system's state space. It guarantees that the system can never reach an unsafe state, no matter what adversarial inputs are fed into the matrix.

AI as the Assistant (and the Supply Chain Risk)

If verifying the AI brain itself is that intense, what happens when that same AI is actually out there writing traditional code?

That's the second part of the paradox.

If Large Language Models are suddenly generating code a hundred times faster than human engineers, the sheer volume alone breaks our current auditing methods. It's like hiring a super-fast construction crew to build a skyscraper. They work at lightning speed, but they occasionally try to use painted cardboard instead of steel beams. Because the cardboard mathematically looks like steel to their pattern-matching algorithms, our building inspectors (our verification methods) need an entirely new framework to catch that cardboard before the concrete is poured.

That incredible speed exponentially amplifies supply chain risk. AI assistants write code by rapidly pulling in open-source libraries, dependencies, and snippets from across the internet. The attack surface for compromised code becomes massive. That "cardboard beam" might have been slipped into the supply chain on purpose by a malicious actor.

This is why provenance frameworks are no longer optional.

We're talking about frameworks like SLSA (Supply-chain Levels for Software Artifacts) and SBOMs (Software Bill of Materials). And these aren't just simple checklists or readmes. They are cryptographically signed attestations. Every single time a piece of code is compiled, the system hashes the exact version of the compiler used, the specific libraries imported, and the exact build environment. It creates an unbroken, cryptographic chain of custody so you know exactly where everything came from.

Regulators and enterprise buyers are treating this as the absolute minimum baseline. If you cannot cryptographically prove exactly where every byte of your software originated, no one even begins the conversation about whether the code itself is mathematically sound.

The Evidence Spectrum

Assuming our cryptographic supply chain is locked down, we still have to prove the code actually does what it's supposed to do.

Let's look at the actual tools our "building inspectors" are using. There is an entire taxonomy of verification called the 'Evidence Spectrum,' and the rigor of these tools varies wildly.

At the very top is Interactive Theorem Proving and SMT (Satisfiability Modulo Theories) Solvers — tools with names like Roc, Lean 4, and CVC5. Theorem proving sounds like a mathematician at a chalkboard, but we are talking about millions of lines of code. What an SMT solver does is reduce the software to pure algebraic logic. Imagine translating a function in your code into a massive, highly complex Boolean equation. It's pure math.

The solver then uses heavy algorithmic heuristics to try and find a single variable assignment — a single set of inputs — that would make the equation false (which represents a bug or a violation of your specification). If the solver exhaustively proves that the formula is unsatisfiable, meaning it couldn't find a single way to break it, then no combination of inputs can ever violate the specification. You get a literal mathematical proof that your code is functionally correct.

The big catch? This requires you to write a perfectly rigid mathematical specification first. You have to translate human intent into algebra. For massive, highly concurrent systems like an operating system, an SMT solver would just choke on the infinite complexity.

That limitation brings us to the next tier: model checking, using tools like TLA+ or nuXmv. Where theorem proving tries to mathematically solve the code itself, model checking explores the state space of a system's design. If theorem proving is like writing a mathematical proof for the physics of a maze, model checking is brute-forcing the maze itself — running a computer down every single possible hallway to ensure there are no dead ends. Systems like TLA+ look at discrete math models of the system's architecture to find fundamental logic flaws, like race conditions, before a single line of code is even written.

And then there is Cryptographic Verifiable Computation, like zkVMs (zero-knowledge virtual machines). These prove execution integrity. If you send a massive dataset to a third-party server to run a complex algorithm, a zkVM executes the code while simultaneously generating a cryptographic trace of the execution — a mathematical receipt. The "zero-knowledge" aspect means you can verify this receipt mathematically without the server ever having to reveal the underlying proprietary data. You prove the execution happened flawlessly while keeping the inputs entirely secret.

Layered Assurance and Runtime Safety

Even with all this math guaranteeing perfection, the overarching posture today is 'Layered Assurance,' which heavily involves 'Runtime Assurance.'

Setting up a runtime monitor isn't admitting defeat; it's an admission of reality. You simply cannot formally verify every single component of a modern dynamic system, especially when dealing with the probabilistic nature of AI interacting with the messy real world.

Layered Assurance is about pragmatic risk management. You use interactive theorem proving for tiny critical security kernels, model checking for system architecture, and for massively complex AI controllers, you use Architectural Containment (Runtime Assurance).

Look at the high-stakes case study from NASA Langley regarding autonomous drones. They wanted to use advanced, unverified AI to fly aircraft. You can't just trust a black-box AI on its own. So, NASA utilized a runtime assurance architecture known as Simplex.

In Simplex, the unverified AI acts as the primary controller because it's great at optimizing routes. However, running parallel to it is an internal monitor and a highly simplified, formally verified backup controller. It's exactly like a student driver in a car. The AI is the teenager handling the steering wheel, and the runtime assurance monitor is the driving instructor with a secondary brake pedal. If the AI crosses a hard mathematical boundary, the instructor slams the brake and takes over. The real engineering challenge was using formal theorem proving to mathematically derive exactly how fast the drone's sensors needed to sample data so the "instructor" could react before the physics of the drone became unrecoverable.

We see this same rigor in medical devices. For an autonomous Artificial Pancreas system, researchers didn't test their way to safety. They translated the entire system's design diagrams into a formal state model using nuXmv, writing 132 formal specifications derived from clinical safety requirements. Very early on, the model checker discovered a direct inconsistency that a human reviewer had completely missed. The math caught a fundamental design flaw before any hardware was built.

In the financial sector, a single logic bug in a smart contract can irrevocably drain billions of dollars. Formal verification tools like the Certora Prover are now an absolute baseline. Auditors write "economic invariants" — properties that must remain true no matter what path the code takes. The SMT solvers try to find any bizarre mathematical loophole that breaks the invariant. If they fail, the institution has mathematical proof the liquidity pool is safe.

The Specification Bottleneck

If we have this incredible arsenal of tools, why isn't every piece of critical software perfectly verified?

It comes back to the human element. The massive bottleneck isn't processing power; it's the specification. Verification tools are incredibly literal. They check if the code matches the specification you wrote. But what if the spec doesn't match what the human engineer actually intended to build?

Microsoft Research calls this the "intent formalization problem." Human intent is messy, ambiguous, and context-dependent. Translating human desire perfectly into rigid, mathematical logic is incredibly difficult.

Think of it like the mythological genie in the lamp. The problem is almost never that the genie (the verified code) fails to grant your wish. The problem is that human wishes are ambiguous, and the genie executes the literal, mathematical exactness of your specification. You ask for a million dollars, and the genie crushes you under a mountain of pennies. The code functioned perfectly according to the spec; the specification was just fatally flawed.

To solve this, there is a massive push to use AI to bridge the gap between human intent and formal math. Agentic frameworks like LioDojo and Apollo utilize 'verifier-guided repair.' The LLM writes a draft mathematical specification, feeds it to the rigid verifier, and the verifier inevitably finds a logic error and feeds it back to the LLM. It is a continuous, high-speed dialogue between the creative engine of the AI and the rigid truth engine of the verifier.

But there is a logical trap: If we rely on LLMs — which we know hallucinate — to write our foundational specs, aren't we just shifting the hallucination problem one step to the left? You might have a 100% mathematical guarantee that the code matches the spec, but if the AI injected a subtle flaw into the spec itself, the entire foundation is compromised.

To mitigate this, you have to demand checkable evidence artifacts that are completely independent of the AI. You can't trust a black-box LLM, and you shouldn't blindly trust a massive SMT solver either, because solvers are software too. This is why the industry is moving toward tools like CVC5 that export step-by-step mathematical proofs. You take that proof and feed it into a highly trusted, incredibly small piece of software called a kernel that humans can audit manually. Trust nothing unless it provides a cryptographic or mathematical receipt that can be independently audited.

Redefining Certainty

Whether you are a project manager evaluating enterprise tools, an engineer designing a new system, or just someone navigating a digital world, "assurance" is no longer just a checkbox on a testing spreadsheet.

The only defensible engineering posture today is the layered assurance matrix. You use model checking to catch architectural flaws, SMT solvers on critical security components, runtime assurance safety envelopes around unpredictable AI models, and cryptographic SBOMs to prove supply chain integrity. It is an interlocking ecosystem of trust.

The big takeaway here is to stop demanding specific testing tools. Technology moves too fast. Instead, demand acceptable evidence artifacts. Demand to see the formal models, the exported mathematical proofs, the runtime reaction calculations, and the cryptographic hashes. Focus on the irrefutable evidence.

But there's one deeply sobering final thought to ponder. We are moving toward a future where human engineers can no longer fully comprehend the AI-generated code running our critical systems, and they also cannot fully comprehend the massive mathematical proofs generated by machines to verify that code.

At what point does human understanding become the actual bottleneck for truth and trust in our technology? The math might be perfect, but our biological ability to understand it is hitting a wall. When the code is a black box, and the math verifying it is too vast for the human mind to hold, we have to fundamentally redefine what it means to be certain.

Executive Summary

Provable and verifiable software comprises a spectrum of techniques that can produce machine-checkable evidence that a program, model, or system satisfies a formally stated property.

Today, this spectrum is expanding in two directions at once:

(i) traditional formal methods (theorem proving, model checking, SMT-backed deductive verification, abstract interpretation, runtime verification) are gaining stronger automation and better tooling, and

(ii) cryptographic verifiable computation and "verify-the-AI" techniques are becoming practical for high-stakes settings where computation is outsourced or model behavior must be audited. [1]

AI is changing the verification landscape in three fundamental ways. First, AI is becoming part of the systems we must assure: deep neural networks, learned controllers, and LLM-based agents create new verification targets (robustness, reachability, specification conformance under uncertainty). Competitive benchmarking (e.g., VNN-COMP) and tool development show clear progress, but also highlight remaining scalability gaps and benchmark-dependent performance variability. [2]

Second, AI is increasingly used to help verification itself: LLM- and retrieval-augmented systems are being built for theorem proving (notably in the Lean ecosystem) and for specification or intent formalization, but strong results typically require tight feedback loops with verifiers, curated datasets, and careful repair/verification of generated artifacts. [3]

Third, the supply-chain and provenance problem is now inseparable from software assurance: AI-assisted coding amplifies dependency risk and artifact tampering risk, raising the importance of provenance frameworks such as SLSA and operational adoption of SBOM practices (including updated U.S. government guidance). These do not "prove correctness," but they are increasingly viewed as the minimum substrate for trustworthy software distribution and auditability. [4]

The most defensible engineering posture today is layered assurance: use formal specification and model checking early to eliminate design errors; apply deductive verification or bounded model checking where code-level guarantees are needed; add runtime verification and runtime assurance architectures to contain unverified/AI components; and apply cryptographic verifiable computation where the threat model includes untrusted execution (e.g., outsourced inference, multi-party computation). The "best" approach depends primarily on (a) what property you need, (b) what abstractions you can tolerate, and © what evidence is acceptable to regulators or auditors. [5]

Definitions and Taxonomy

The terms "provable" and "verifiable" are often used interchangeably, but it helps to separate what is being assured (software behavior, model behavior, computation result) from how evidence is produced (proofs, exhaustive search, over-approximation, monitoring, or cryptographic arguments). This taxonomy is both conceptual and operational: in real toolchains, multiple methods are composed.

Formal verification (broad umbrella). Formal verification is the use of mathematically defined models/specifications and sound reasoning procedures to establish that a system satisfies properties (or to produce counterexamples). Tools span interactive theorem proving, automated theorem proving, model checking, deductive verification, abstract interpretation, and runtime verification. [6]

Interactive theorem proving (ITP) and proof assistants. Systems such as the Rocq Prover (formerly Coq) are designed to develop machine-checked proofs and, importantly for software assurance, to formalize specifications and prove programs comply with those specifications. [1]

Provable guarantees (deductive program verification). "Provable" typically means there exists a formal specification and a proof (often machine-checked) that an implementation satisfies it, under a defined semantics. In "verification-aware" languages such as Dafny, specifications are embedded as contracts and used by an automated verifier. [7]

Model checking (state-space exploration). Model checking explores (explicitly or symbolically) the behaviors of a model to check temporal and safety properties; it is highly automated but often limited by state explosion. TLC for TLA+ is an example of explicit-state model checking for a subset of TLA+. [6]

SMT solving (backbone automation). Satisfiability Modulo Theories solvers decide satisfiability of logical formulas over theories (bit-vectors, arrays, arithmetic, etc.) and serve as automation engines for deductive verification and model checking. cvc5 explicitly supports broad SMT-LIB theories and "beyond SMT" features (e.g., higher-order reasoning, synthesis), and it can produce proofs in multiple formats. [8]

Abstract interpretation and sound static analysis. Abstract interpretation computes over-approximations of program behavior to prove absence of certain classes of errors (often soundly, but potentially with false alarms). In the Frama-C ecosystem, the Eva plug-in automatically computes sets of possible values and warns about possible run-time errors; the WP plug-in uses weakest precondition reasoning over ACSL annotations. [9]

Runtime verification (monitoring traces against specs). Runtime verification evaluates execution traces against formal specifications, trading exhaustive guarantees for practical deployment and coverage over real executions (tests, production telemetry). [10]

Runtime assurance (architectural containment of untrusted components). A closely related concept, especially relevant to AI components, is runtime assurance architectures (e.g., simplex-style switching to trusted controllers) that monitor safety properties and intervene during operation. [11]

Probabilistic verification. Probabilistic model checking extends model checking to systems with probabilistic behavior (Markov chains, MDPs), with properties expressed in probabilistic temporal logics. PRISM explicitly defines this modeling-and-logic workflow as the basis for probabilistic model checking. [12]

ML verification (neural network verification and robustness). Neural network verification tries to establish that a network satisfies a property (commonly robustness to bounded perturbations or safety constraints in a control setting). Empirical evaluations emphasize that tool performance is instance-dependent and that no single method dominates across all realistic cases. [13]

Verifiable computation (cryptographic guarantees). Verifiable computation provides cryptographic evidence that a computation was executed correctly (sometimes with zero-knowledge privacy). zkVMs (e.g., RISC Zero) exemplify this: executing a program yields an output plus a receipt/argument of correct execution. ZKML research focuses on applying ZK proofs to verifiable training/inference/testing, trading significant overhead for strong auditability and privacy properties. [14]

Recent Advances in Theory, Tools, and Practice

Over roughly 2021–2026, the most consequential advances are not only algorithmic; they are also about interfaces, proof artifacts, and integration — the "last mile" needed to turn formal methods into repeatable engineering practice.

timeline
    title Milestones shaping provable & verifiable software (2014–2026)
    2014 : Industrial TLA+ experience report for large-scale systems design (AWS)
    2021 : Frama-C positioned as collaborative industrial-scale C analysis (CACM article)
    2022 : Storm tool paper consolidates high-performance probabilistic model checking
    2023 : LeanDojo creates open toolkits/benchmarks for ML-assisted theorem proving
    2024 : Marabou 2.0 system description : VNN-COMP continues standardization (ONNX, VNN-LIB)
    2025 : Rocq Prover 9.0 completes renaming from Coq : AWS publishes updated correctness practices
    2025 : SpecGen (ICSE) uses LLMs to generate formal program specifications (research direction)
    2026 : Sledgehammer documentation updated : ongoing work on probabilistic model checking ecosystem (Storm)

timeline
    title Milestones shaping provable & verifiable software (2014–2026)
    2014 : Industrial TLA+ experience report for large-scale systems design (AWS)
    2021 : Frama-C positioned as collaborative industrial-scale C analysis (CACM article)
    2022 : Storm tool paper consolidates high-performance probabilistic model checking
    2023 : LeanDojo creates open toolkits/benchmarks for ML-assisted theorem proving
    2024 : Marabou 2.0 system description : VNN-COMP continues standardization (ONNX, VNN-LIB)
    2025 : Rocq Prover 9.0 completes renaming from Coq : AWS publishes updated correctness practices
    2025 : SpecGen (ICSE) uses LLMs to generate formal program specifications (research direction)
    2026 : Sledgehammer documentation updated : ongoing work on probabilistic model checking ecosystem (Storm)

The timeline items above reflect: early major industrial experience with TLA+; industrial-scale C analysis tooling; maturation of probabilistic model checking; open infrastructures for AI-assisted theorem proving; accelerated development in neural network verification; and increased attention to specification generation and supply-chain verifiability. [15]

Key advances by area:

Trustable automation via proof production and reconstruction. A long-standing concern is the trusted computing base: if an SMT solver "proves" a claim, can that proof be independently checked? cvc5's proof production support and export formats (e.g., Alethe/LFSC) illustrate a shift toward checkable evidence. [16] A concrete practice-facing step is Isabelle's ongoing work to reconstruct SMT proofs (including adapting cvc5 outputs for reconstruction), which is explicitly motivated by internal re-proving of externally found results. [17]

Stronger ecosystems around probabilistic verification. Storm's tool paper describes probabilistic model checking as extending traditional model checking to systems with random phenomena and supports using Storm as a library (including APIs). [18] A 2026 overview emphasizes rapid prototyping and interfacing (notably via Python) as part of modern probabilistic model checking workflows. [19] PRISM's documentation continues to represent the "model + temporal logic properties + automated analysis" idiom as the core concept, and contemporary surveys emphasize applications in autonomy and decision-making under uncertainty. [12]

Neural network verification maturing through standardization and competitions. VNN-COMP 2024 explicitly describes standardization efforts: ONNX for networks and VNN-LIB for specifications, plus equal-cost evaluation infrastructure, with multiple benchmark suites and participating teams. [2] System descriptions for major verifiers (e.g., Marabou 2.0) show continuing engineering investment to broaden applicability and performance. [20] Independent assessments (e.g., in JMLR) stress that robustness verification remains highly instance- and method-dependent, supporting a "portfolio thinking" approach rather than expecting a single dominant verifier. [13]

AI-assisted theorem proving shifting from demos to reproducible toolchains. LeanDojo argues that prior methods were hard to reproduce due to private code/data and compute barriers, and proposes an open playground with datasets and retrieval-augmented proving. [3] Newer agentic frameworks (e.g., APOLLO) represent a pattern: compiler/verifier-guided repair and structured search rather than naive sampling, aiming for better efficiency and correctness. [21] In parallel, studies of LLMs in proof/verification settings stress that effectiveness is nontrivial and must be measured in mature projects and workflows, not only curated benchmarks. [22]

Verification-aware languages and LLMs confronting the "intent formalization" problem. Verification-aware languages make checking implementation-vs-spec mechanical, but the harder question is whether the specification reflects the user's intent. Microsoft Research explicitly frames user-intent formalization as a core challenge and investigates LLM-driven approaches in this space. [23] On the specification side, ICSE 2025's SpecGen proposes LLM-driven formal specification generation, reflecting a broader movement toward "specification mining" using modern models. [24]

Cryptographic verifiability moving from theory to engineering platforms. zkVMs (e.g., RISC Zero) are positioned as general-purpose verifiable computing platforms that can prove correct execution of programs and support multiple source-language toolchains compiled to a target ISA. [25] A 2025 survey of ZK-proof-based verifiable ML organizes the area into verifiable training/inference/testing and documents a rapidly growing body of work, underscoring that "verifying AI" can mean cryptographic attestation of computations in addition to semantic verification. [26]

Comparative Landscape of Major Tools and Frameworks

The practical question is rarely "Should we do formal verification?" but rather "Which combination of tools yields the right evidence at acceptable cost and with manageable risk?" A useful comparison is along five axes the user requested: capabilities, languages supported, scalability, automation level, and AI integrations (whether built-in or emerging).

Two cross-cutting observations emerge from this matrix:

First, evidence types differ. Proof assistants aim for kernel-checked proofs; SMT solvers increasingly provide proof objects; model checkers provide counterexample traces; abstract interpretation provides sound over-approximations; runtime verification provides execution-time conformance evidence; cryptographic tools provide computational receipts. These are not interchangeable: regulators and high-assurance reviewers often care about the auditability of the evidence as much as the result. [16]

Second, AI integration rarely means "LLM inside the verifier." Instead, AI most often appears as (i) a front-end for specification drafting, tactic generation, or search guidance, and (ii) a target requiring specialized verification methods (neural network robustness, runtime assurance around black boxes). [3]

Case Studies in Safety-Critical Domains

Safety-critical verification is best understood through concrete outcomes: what properties were verified, what bugs or inconsistencies were found, and what organizational lessons emerged.

Autonomy

A representative autonomy pattern is verifying learned components as part of a larger control architecture. One peer-reviewed example (shared-control autonomous driving) reports a formally verified neural network predictor for takeover time (a human-in-the-loop safety function), illustrating that verification targets can be embedded in ML-assisted autonomy, not only end-to-end driving stacks. [27]

A more systems-oriented pattern is code-level compositional verification for automated driving controllers. CoCoSaFe is presented as a compositional code-level safety verification framework that uses compositional contracts and bounded model checking for subsystem verification and includes a decomposition method for neural-network-based controllers; it reports effectiveness on adaptive cruise and lane-keeping controllers (traditional and NN-based). [28]

Lessons for autonomy: (i) the specification/contract boundary must be carefully chosen so that NN verification is applied to components with tractable interfaces, (ii) decomposition and compositional contracts are central to scalability, and (iii) verification often mixes several methods (contracts + BMC + a neural network verifier) rather than relying on a single tool. [28]

Aerospace and aviation-adjacent autonomy

Aviation highlights a second pattern: assure the integration of untrusted/AI components via runtime assurance architectures. A NASA Langley paper on "runtime assurance of autonomous UAS" describes Runtime Assurance (RTA) as a design-time architecture where an internal monitor acts on detecting property violations, with simplex architectures switching control from an untrusted controller to a trusted controller upon safety property violation. The paper explicitly frames simplex RTA as a method for integrating AI/ML and other unverified software into safety-critical aircraft operations. [11]

This case also illustrates a rigorous tooling approach: formal verification of the simplex RTA framework in the language of hybrid programs, supported by a tool that embeds reasoning about hybrid programs in a theorem-proving environment, and deriving requirements such as sensor sampling rates needed to check the relevant switch property. [11]

A complementary aerospace domain story is certification-oriented formal methods. NASA's DO-333 case study report summarizes three case studies (theorem proving, model checking, abstract interpretation) as evidence patterns to satisfy certification objectives for an avionics example (a dual-channel flight guidance system), emphasizing how formal methods can be used as part of certification evidence even if they do not constitute "complete certification by proof." [29]

Lessons for aerospace: (i) formal methods can produce arguments and constraints (e.g., monitoring rates) that directly shape system design; (ii) runtime assurance offers an architectural bridge when full verification of an AI controller is infeasible; and (iii) certification-aligned evidence typically requires traceability from requirements to formal artifacts and tool qualification considerations, not only a technical proof. [11]

Medical devices

Medical devices highlight a third pattern: model-based verification of complex software-dependent systems and catching design/model inconsistencies early. A 2022 case study translates SysML activity/state machine diagrams into a nuXmv model for an Autonomous Artificial Pancreas System (AAPS) and uses formal validation and verification against a set of specifications derived from safety requirements. [30] The authors report 132 total specifications spanning validation and verification, with 105 used for validation and 29 for verification, and provide summary tables indicating passing results. [30] They also describe discovering an inconsistency between an activity diagram and the broader model flow via a failed validation specification and then reconciling model/spec expectations. [30]

On the regulatory side, the U.S. FDA recognizes IEC 62304 (2006 + A1:2015) as a consensus standard defining life cycle requirements for medical device software, framing engineering obligations around lifecycle processes and maintenance. [31] The FDA has also issued cybersecurity guidance for medical devices that shapes what manufacturers provide in premarket submissions, reinforcing that assurance is not only functional correctness but also security posture and operational risk controls. [32] For AI-enabled device software functions, the FDA published draft guidance (January 2025) describing lifecycle management and marketing submission recommendations (non-binding, not for implementation), and the associated Federal Register notice clarifies that when finalized it is intended to guide submission contents and risk management across the total product lifecycle. [33]

Lessons for medical: (i) formal verification can detect inconsistencies between requirements representations and behavioral models, (ii) validation specs are as important as "verification specs" because they check model fidelity to intended behavior, and (iii) assurance must align with lifecycle-oriented regulatory expectations — especially for AI-enabled functions where post-market change and monitoring become central concerns. [30]

Finance and high-stakes digital assets

In finance, two "verification" meanings dominate today: (i) formal verification of smart contracts and protocols, and (ii) cryptographic verifiable computation for correctness and auditability of off-chain computation.

Formal verification for smart contracts is increasingly operationalized as industrial practice. A prominent example is the Certora Prover, which is marketed around automated verification given user-written specifications and producing counterexample scenarios when properties fail. [34] Publicly posted formal verification reports show its application to real protocols, such as the Aave V3 Risk-Steward contracts, combining formal verification and manual security assessment. [35] Research also emphasizes domain-specific property challenges: for example, work on verifying liquidity properties (e.g., whether a sequence of transactions can always withdraw a given amount) argues that existing tools struggle to express and verify such properties, motivating specialized approaches. [36]

On the cryptographic side, zkVM platforms explicitly target "verify anything" computation models. RISC Zero describes producing cryptographic receipts of correct execution for RISC-V binaries and positions the model as general verifiable computation. [14] Surveys of ZK-proof-based verifiable ML show how these techniques can extend to verifiable inference/testing/training, which is particularly relevant for financial settings that require auditability without disclosing proprietary data or models. [26]

Lessons for finance: (i) specifications must capture economic and liquidity invariants, not only functional correctness; (ii) counterexample generation is critical for developer iteration; and (iii) cryptographic verifiability is becoming a parallel assurance channel when trust boundaries include third-party execution environments. [34]

Interactions Between AI/ML and Formal Methods

The AI–formal-methods interface now has at least four distinct sub-areas, each with different maturity and risk profiles.

Using AI to aid verification (automation of proofs/specs). In theorem proving, LeanDojo frames the primary bottlenecks as reproducibility barriers and premise selection, proposing an open toolkit and retrieval-augmented prover. [3] APOLLO (NeurIPS 2025) exemplifies a broader shift toward verifier-guided repair: use the proof assistant's compiler/feedback as an oracle to iteratively repair LLM outputs under constrained budgets. [21] In verification-aware programming, research explores both intent formalization and verified code synthesis: Microsoft Research explicitly discusses the gap between mechanical checking and ensuring a specification matches user intent, while separate work studies LLM-driven synthesis of verified Dafny methods. [23] In specification mining/generation, SpecGen (ICSE 2025) proposes LLM-driven formal specification generation for Java programs, reflecting an emerging tool class: not a verifier, but a "specification producer" that can feed verifiers. [24]

Verifying ML models (robustness, reachability, and safety constraints). Competitions and benchmarks have become central to this subfield. VNN-COMP 2024 describes standard formats (ONNX, VNN-LIB) and an evaluation pipeline enabling objective comparisons, which is essential because verifier performance is sensitive to both properties and network architectures. [2] Independent evaluations in JMLR stress the diversity of methods (MILP, SMT, abstract interpretation, GPU-based methods) and report systematic performance analyses across many networks and properties, concluding that suitability depends on instance characteristics rather than offering a single universal winner. [13] Tool descriptions (Marabou 2.0; NNV 2.0; NeuralSAT; α,β-CROWN) show rapidly evolving engineering, but also reinforce that "verified" typically means verified relative to encoded approximations, bounds, and query semantics. [20]

Robustness vs. specification alignment. For ML-enabled systems, robustness (e.g., local perturbation robustness) is only one dimension; real systems require specifications that connect ML outputs to system-level safety constraints. The trend toward system-level benchmarks (e.g., NN4SysBench for NN components in computer systems) reflects recognition that verification targets are no longer just image classifiers but networks embedded in broader infrastructures. [37]

Runtime assurance as a bridge for black-box AI. When ML models are too complex to verify fully, runtime assurance architectures can provide safety envelopes or fallback strategies. NASA's simplex RTA framing explicitly targets integration of AI/ML components into aircraft operations by monitoring properties and switching to trusted controllers. [11] This pattern generalizes: assurance becomes a combination of formal offline reasoning about the monitor/controller logic and runtime enforcement over the untrusted ML component.

Cryptographic verification of AI computations (ZKML / proof of inference). ZKML research focuses on proving that training or inference was done correctly without revealing private inputs or proprietary weights. A 2025 survey organizes the field into verifiable training/inference/testing and highlights implementation challenges and directions. [26] zkVMs can serve as engineering substrates for this by shifting the verification target from "semantic correctness of the model" to "correct execution of the specified inference computation," which is useful for audit and compliance but does not by itself guarantee that the model is safe or fit for purpose. [14]

Limitations, Open Problems, and Research Directions

Despite visible progress, the "current state" is still best described as capable but uneven — strong in some classes of properties and systems, fragile in others, and frequently bottlenecked by specification and scalability.

Specification remains the dominant bottleneck. Verification-aware languages reduce the gap between code and spec checking, but the hardest step is ensuring the specification captures user intent; Microsoft Research calls out the lack of an algorithmic way to guarantee correctness of user-intent formalization. [23] LLM-based spec generation (e.g., SpecGen) is promising, but it shifts risk: the system can now generate plausible specifications that might be wrong or incomplete, requiring verification of the specification itself (or at least robust review and traceability). [24]

Scalability is a structural constraint, not just an engineering issue. In neural network verification, both competitions and independent benchmarks show that different verifiers excel on different benchmark families and that some benchmarks remain unsolved by leading tools, reflecting theoretical and computational hardness as well as engineering gaps. [2] In classical model checking, state explosion remains fundamental; modern tooling mitigates it with symbolic methods, bounded checking, cloud scaling, and compositionality, but the limitation is not removed. [38]

Trustworthiness of automation depends on checkable artifacts. A recurring research direction is reducing reliance on large, complex solvers as untrusted oracles by producing proofs that can be independently checked. cvc5's proof production and export formats represent this trend, and Isabelle work on SMT proof reconstruction illustrates its practical value. [16] Similar motivations appear in neural network verification research that develops certified checkers for verification artifacts, aiming to strengthen confidence beyond "tool says SAT/UNSAT." [39]

Probabilistic guarantees and distribution shift are hard to formalize. Probabilistic model checking provides rigorous analysis for stochastic models, but building faithful models of real-world uncertainty (and mapping them to meaningful properties) remains challenging; surveys of probabilistic model checking for autonomy emphasize both the promise and the complexity of multi-objective, uncertain settings. [40] For ML systems, distributional shift can invalidate robustness assumptions; formalizing "robust under deployment conditions" often requires modeling assumptions that are difficult to justify. [13]

Tool usability and organizational fit remain barriers. Industrial TLA+ experience reports and literature reviews emphasize that tools are valuable for debugging designs but can remain ad hoc/grassroots and depend heavily on internal expertise and culture. [38] Runtime verification similarly faces adoption barriers related to instrumentation overhead, specification maintenance, and developer workflow integration, motivating ongoing research on overhead reduction and evolution-aware monitoring. [10]

Software supply-chain assurance is now part of verification's threat model. Even perfectly verified source code is undermined if build and distribution pipelines are compromised. SLSA explicitly frames supply-chain levels (provenance, tamper resistance, and incremental controls) as a consensus-driven specification for improving supply chain security. [4] SBOM guidance (including updated draft guidance and definitions from U.S. agencies) frames SBOMs as formal records of components and relationships, enabling vulnerability response and procurement requirements. [41]

Research directions that plausibly matter most for the next 3–7 years follow directly from these limitations: scalable compositional reasoning (especially for ML-enabled systems), better specification engineering (including human-in-the-loop and traceability), proof-carrying results from solvers and verifiers, and integrated assurance that spans source → build → artifact → runtime telemetry. [16]

Practical Recommendations for Engineers and Policymakers

The recommendations below are framed as decision rules rather than tool evangelism, because assurance is fundamentally a risk-management activity.

Recommendations for engineers

Adopt a layered workflow that matches properties to methods:

• Start from design-level specification when concurrency/distribution or safety envelopes dominate. TLA+ is explicitly positioned as eliminating fundamental design errors via precise modeling and TLC model checking, and industry experience emphasizes its value for debugging designs. [6]

• Use bounded model checking (CBMC) or symbolic model checking (nuXmv) when you need automated counterexamples and can accept boundedness or an abstract model. CBMC's definition explicitly centers on proving safety of assertions under bounds via bit-precise translation and loop unrolling; nuXmv provides symbolic checking with SAT/SMT-based engines. [42]

• Use deductive verification (Dafny, SPARK, Frama-C WP) when correctness depends on data structure invariants, functional properties, or absence of runtime errors and you can invest in specifications/contracts. Dafny's design (contracts + automated verifier) is explicit in its reference docs; SPARK's proof materials describe generating verification conditions; Frama-C WP is explicitly about proving ACSL annotations using external decision procedures. [7]

• Add sound static analysis (Frama-C Eva) early in C codebases to detect runtime error classes and guide where deeper proofs are needed, since Eva is designed to compute possible value sets and warn about runtime errors. [9]

• For ML-enabled components, separate "verify the model" from "verify the system." Use neural network verifiers (Marabou, α,β-CROWN, NeuralSAT, NNV) for well-scoped properties (robustness, bounded reachability), informed by competition and benchmark evidence; apply system-level contracts and compositional reasoning (as in CoCoSaFe) to make the overall verification tractable. [2]

• When full verification of AI components is infeasible, implement runtime assurance patterns (monitors + fallback trusted controllers) as a pragmatic safety envelope — an approach explicitly discussed for integrating AI/ML into safety-critical aircraft operations. [11]

Treat AI assistance as an accelerant, not an oracle:

• Use LLMs for first drafts of specs/proofs/contracts, but require verifier feedback, proof reconstruction, and human review. The major successful patterns (LeanDojo, APOLLO) rely on tight verifier-in-the-loop processes rather than unchecked generation. [3]

• Prefer checkable evidence: proof-producing solvers (cvc5) and proof reconstruction in proof assistants reduce the trusted surface area, which is increasingly important as toolchains incorporate more automation and potentially AI-generated artifacts. [16]

Incorporate supply-chain controls as part of "verification done":

• Align build pipelines to SLSA levels and generate provenance; require SBOMs for critical deployments and vendors, since these are increasingly codified as minimum expectations for software transparency and risk management. [4]

Recommendations for policymakers and regulators

Policy levers should focus on evidence requirements and process traceability, not mandating specific tools:

• For high-risk sectors, specify acceptable assurance artifacts: formal models/specs for critical algorithms, proof or bounded-check evidence for key safety invariants, runtime monitoring/assurance plans, and post-market change control processes for AI-enabled software functions. FDA guidance documents explicitly frame lifecycle management and submission documentation for AI-enabled device software functions as part of regulatory evaluation. [43]

• Require baseline supply-chain transparency (SBOM) and provenance maturity (SLSA-like practices) for government procurement and critical infrastructure, since U.S. agencies explicitly define SBOMs as formal records of components and relationships, and publish updated minimum element guidance. [41]

• Encourage standardization efforts that improve reproducibility and comparability of verification results, similar to how VNN-COMP standardizes formats and evaluation pipelines for neural network verification tools. [2]

• Invest in tool qualification guidance and workforce development where formal methods intersect with certification (e.g., avionics-oriented case study evidence for DO-333 style objectives), emphasizing repeatable evidence production rather than "trust us" claims. [29]

A reference verification workflow

This workflow reflects the dominant contemporary practice: iterative refinement via counterexamples and proof failures, layered with runtime controls and supply-chain evidence to address both semantic correctness and operational trust boundaries. [6]