The Trust Problem Has Shifted: What Formal Verification Can and Cannot Guarantee About AI-Generated Code

What formal methods are

At their core, formal methods solve a problem that is simple to state. You have a program. You have a formal specification — a precise description, written in mathematically rigorous terms, of what that program is supposed to do. A verification system attempts to prove that the program satisfies the specification.

Consider one step of a flight-control loop that decides whether to command an automatic correction:

def update_control(sensor, actuator):
    reading = sensor.read()
    if reading > THRESHOLD:
        actuator.correct()
    else:
        actuator.hold()

One specification might require a local control property: the actuator is commanded only when the measured value exceeds a threshold. A stronger specification might bound the authority of the controller: it cannot repeatedly issue corrections beyond a safe limit. A still stronger specification might require fault tolerance: the controller must not take unsafe action when sensor readings are unreliable or disagree.

All three properties can be stated formally as specifications, but they provide very different levels of assurance and proving them may require different proof strategies. Formal methods are ultimately about proving that a program satisfies a specification encoding the expected behavior of the program or a particular property worth guaranteeing.

The specification is therefore the ground truth on which the verification effort is based. Formal verification only makes sense if the specification is clearly stated and correctly reflects the intended behavior. The statement “This code is formally verified” only makes sense with respect to a given specification.

Why software verification is harder than mathematical proofs

The recent success of proof assistants such as Lean, Rocq, and Isabelle has made machine-checked proof feel increasingly within reach, particularly among mathematicians. These tools allow users to state definitions and theorems in a formal language, construct proofs with varying degrees of automation, and have those proofs checked by a small trusted kernel. In mathematics, there is a good reason for optimism around such tools. Mathematicians largely share a common language of definitions, axioms, and logical inference rules. Once a theorem is expressed in the language of the proof assistant, that same language provides a uniform environment for checking whether the proof is valid.

Software is different.

Returning to the flight-control example, verifying the same logic in Rust, Python, C++, or Octave is not a matter of pressing the same button four times. Each language often requires its own semantic model and reasoning logic, and therefore its own verification tool. A Rust proof may need to reason about ownership, borrowing, lifetimes, and panics. A C++ proof may need to account for undefined behavior, aliasing, templates, and low-level memory manipulation. A Python proof may need to account for dynamic dispatch, implicit conversions, native libraries, numerical behavior, and runtime-dependent behavior.

In the real world, programs are written in many languages, each with its own semantics, libraries, runtime systems, compilation strategies, and interactions with hardware. Before one can prove anything about a program, one must first define precisely each of these components. Even the same-looking program can mean different things in different languages. For example, x + 1 > x is true for every integer in Python, whose integers have arbitrary precision. In C++, the analogous expression over int is only meaningful when x + 1 does not overflow. A verifier for the Python program and a verifier for the C++ program are not proving the same fact about the same mathematical object — they are reasoning about two different language semantics.

A formal verifier is therefore not a general artifact that can simply be pointed at arbitrary code. It must understand the semantics of a particular language: its type system, memory model, concurrency primitives, exception behavior, standard libraries, and edge cases. Furthermore, languages evolve over time and these tools must keep up with these changes.

Over the last two decades, the programming languages and formal methods communities have made enormous progress. Tools such as Dafny, Why3, Verus, Viper, Kani, CBMC, and ESBMC have dramatically expanded the set of programs that can be verified with reasonable effort. But each tool embodies years of engineering and research. Each is built around particular languages, styles of programming, classes of properties, and proof strategies.

This is why current verification tools, powerful as they are, are still far from universal. They often support carefully chosen fragments of languages, selected libraries, specific classes of properties, or particular programming styles. That is not a criticism; it is how progress is made on a hard problem. Mainstream language features can hide surprisingly deep complexity (e.g., Java Generics are Turing Complete [1]). If even the type system of a mainstream language can contain this much computational complexity, then building sound, scalable verification infrastructure for full production languages is clearly not just a matter of engineering polish.

There is also a fundamental limit: full program verification is undecidable in general. No tool can take an arbitrary program and rich specification and always determine automatically whether the program satisfies it. This is where LLMs may have a real role to play. Not by making undecidable problems decidable, and not by replacing verification, but by helping with the parts that currently require expert human effort: break complex verification tasks into smaller and more manageable ones, discover useful intermediate lemmas, generate proofs, and suggest ways to recover when a verification attempt fails.

The verifier remains the authority. The model can help produce candidate proofs, but the formal system decides whether those proofs are valid.

What should we verify?

Suppose every programming language had mature verification tooling. Suppose all of these tools interoperated seamlessly. Suppose proofs could be generated automatically and at negligible cost.

The hardest problem would still remain.

What property should we verify?

Since their inception, formal methods have benefited from a simple division of labor. A human wrote the implementation. A human — sometimes a different one — wrote the specification. Verification checked that the two agreed.

This separation mattered. When verification failed, the failure conveyed information. Either the implementation was wrong, or the specification was wrong. In either case, the disagreement revealed something useful.

Much of the confidence provided by verification comes from this redundancy: two independently produced descriptions of the intended behavior must agree.

Large language models weaken that arrangement: they can write the specification, generate the code, and construct the proof connecting them. The verification still produces a green checkmark. What it no longer ensures is correctness.

Returning to the flight-control example, suppose the component reads two redundant sensors. A natural requirement is that it should command a correction when the aircraft is genuinely at a high angle of attack. A model might generate code like this:

def update_control(left_sensor, right_sensor, actuator):
    reading = left_sensor.read()
    if reading > THRESHOLD:
        actuator.correct()
    else:
        actuator.hold()

It might also generate a specification that appears reasonable: the controller commands a correction if and only if reading > THRESHOLD.

The code satisfies this specification exactly. But the specification never constrains how reading relates to the two sensors — so it is silent on disagreement. The implementation above acts on left_sensor alone and ignores right_sensor entirely. A second implementation that averages both sensors, or one that refuses to act when they disagree, would satisfy the same specification while behaving completely differently when a sensor fails. The specification is loose and admits all of these implementations, including the one that drives unsafe control action from a single faulty reading. In this example, the verifier does not fail. It does exactly what it was asked to do.

This is not a hypothetical failure mode. Following the grounding of the 737 MAX, MCAS was redesigned to compare both angle-of-attack sensors, suppress activation when the sensors disagree, and prevent repeated trim commands in response to a single event; the original system relied on input from only one sensor [3]. The redundancy and disagreement-handling requirements omitted by the generated specification are exactly the safeguards that are essential in safety-critical systems.

That specification is true relative to the sensor value. But it says nothing about whether the sensor value is reliable, whether redundant sensors agree, or whether repeated control authority is bounded. The implementation may therefore satisfy the generated specification perfectly while still violating the real safety requirement: a safety-critical controller must not allow a single unreliable sensor input to drive unsafe control action.

This is not solely a theoretical concern. Users often express intent in English, and English specifications are frequently underspecified and not detailed enough. The model must fill in the gaps: which edge cases matter, which invariants are essential, which failures are unacceptable, and which behaviors are merely accidental. Once those choices are made by the model, the user may no longer know exactly what property is being verified.

More critically, models may learn to generate specifications that are easier to satisfy and verify rather than specifications that faithfully capture user intent. This is the specification analogue of reward hacking: optimize the measurable objective while missing the real one. A verifier may then certify exactly the wrong property.

In all these examples, the verifier does not fail. It does exactly what it was asked to do. A proof that code satisfies a specification is only as meaningful as the specification itself.

This is the challenge behind many claims that verification will solve hallucinations. Verification can establish consistency between code and specifications. It cannot automatically establish that either one captures the correct intent.

The trust problem has not disappeared. It has moved.

Formal methods at Code Metal

At Code Metal, our primary application of formal methods is software translation: moving programs from one language, platform, or execution environment to another while preserving their observable behavior. Two important cases are legacy code modernization, where organizations need to migrate valuable existing code into modern languages and infrastructure, and hardware-oriented translation, where software must be transformed and optimized to run efficiently on new targets such as GPUs, NPUs, and domain-specific accelerators.

This setting changes the verification problem in an important way. We are not asking a model to come up with a specification for a newly generated program. Instead, we begin with an existing piece of software and ask whether a translated version preserves its behavior.

The source program becomes the specification and the central property, therefore, becomes proving a form of equivalence.

While equivalence leads to a clear specification, proving it remains a challenging problem. Source and target languages often have different type systems, memory models, standard libraries, numerical behavior, concurrency models, and runtime semantics. Establishing equivalence requires reasoning simultaneously about both sides of the translation and defining exactly which observable behaviors must be preserved.

The advantage is that this definition only needs to be established once for a language pair or translation pipeline. We do not need a human to write a fresh functional specification for every translated program. Instead, we define what it means for programs in the source and target languages to be equivalent, build the infrastructure needed to check that relation, and then apply it.

That focus makes the problem not just more tractable, but more principled. The source program is the ground truth, by definition, and transpilation must preserve its behavior. Correctness is judged against the actual source artifact — not against an arbitrary LLM-generated description of it.

We can use the full arsenal of formal methods rather than treating verification as a single one-size-fits-all technology. Testing quickly identifies obvious translation errors. Lightweight formal methods such as property-based testing, bounded model checking, symbolic execution, and static analysis can eliminate large classes of mistakes before expensive proof generation is attempted. These techniques can also help decompose large translation problems into smaller equivalence-verification tasks that can be solved independently.

For example, static analyses can prove the absence of language-specific failures such as Rust panics, out-of-bounds accesses, or illegal memory behavior. Symbolic execution engines and bounded model checkers can search bounded executions for counterexamples and formally prove equivalence of loop-free programs. Protocol and API checks can ensure that translated code respects required calling conventions, resource lifetimes, or library usage rules.

Only after a translation survives these earlier stages do we invest in stronger equivalence proofs.

This layered approach is essential. Lightweight methods provide scalability and fast feedback. Stronger methods provide assurance where it matters most. Together, they create a practical path toward trustworthy software translation.

For the last step, formally verifying equivalence, we build on decades of work from the formal methods community, and existing tools already let us prove meaningful properties about real translations. More work is needed to scale these guarantees to entire software repositories that exhibit rich language features, and complex execution environments, but the path is clear: combine translation, testing, lightweight formal methods, and proof generation into a single engineering pipeline.

The clear focus of Code Metal’s mission, i.e., applying formal methods to real-world modernization projects, allows us to systematically expose gaps in today’s verification infrastructure. Some languages lack mature verification tooling. Some programming languages or libraries lack formal models. Some target platforms require reasoning about performance, parallelism, or hardware-specific behavior that existing tools were not designed to handle. Closing these gaps requires new tooling, new language support, and continued investment in verification technology.

We are building that infrastructure inside Code Metal, contributing to existing verification ecosystems, and planning to release improvements back to the open-source community where possible. The goal is not to replace the formal methods community’s work, but to operationalize it: to turn decades of research into practical systems that can verify real translations of real software.

Where the market actually is

We believe the largest opportunities for verification are not necessarily in proving arbitrary AI-generated software correct.

They are in domains where specifications already exist or can be stated precisely: software modernization, language translation, compiler correctness, protocol compliance, security properties, infrastructure software, hardware migration, and safety-critical systems.

These markets are less sweeping than the vision of automatically verifying all software generated by AI. They are also far more immediate. Companies already spend enormous sums maintaining legacy systems, migrating codebases, porting software to new platforms, and validating critical infrastructure. In such settings, formal verification does not need to solve every possible correctness problem to be a valuable tool. Its value lies in reducing risk in workflows that already have large budgets, high failure costs, and clear notions of success.

That is where formal methods can deliver value today.

While agents have placed coding in the hands of everyone and made programmers faster, the same level of democratization is not around the corner for formal verification. Prior studies have made it clear that education, tooling, and industrial environment are major barriers to broader verification use [2].

This education problem is especially important in the AI era. The broader dream of general-purpose verified AI-generated software will require a generation of software engineers who are literate in specifications, logic, semantics, and proof. Today, most programmers are not trained to state formal properties, reason about invariants, or understand what a verifier has and has not proved. If formal methods are going to become part of mainstream software engineering, academic programs and industry training will need to close that gap.

To summarize, today verification cannot be a magic solution to hallucination. It is a powerful technology for establishing trust when the property being verified is clear, precise, and independently grounded.

That is where formal methods help AI today. It is also where the next generation of reliable AI-powered software engineering will begin.

References

Authors

Loris D’Antoni is a Professor in the Programming Systems Group at the University of California San Diego and a Scholar at Code Metal. Before joining UC San Diego, he co-founded the MADPL group at the University of Wisconsin–Madison.

Laura Titolo is a Principal Research Scientist at Code Metal and was previously a Lead Research Scientist in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center and a member of the NASA Formal Methods team.