Verified AI and Formal Verification Are Changing Agentic Engineering

I knew formal verification would play a critical role in agentic engineering all the way back in March 2026, and it is in fact happening now. My predictions were correct. Here’s what’s going on and what you need to know.

My iPhone notes dated March 4, 2026 recorded Axiom’s $150 million Series A target and a direction I was watching closely: verified AI and mathematical verification for code generation. Axiom later announced $200 million. That’s $50 million above the target I’d written down.

Selected excerpts from my notes dated March 4, 2026.

My notes connected verified AI and AxiomProver with verification in AI coding workflows.

On March 5, I wrote four words in a conversation with colleagues: “math proofs as verification.”

I was discussing the verification layer of AI-assisted development. I had shared Leonardo de Moura’s essay, When AI Writes the World’s Software, Who Verifies It?, because the implications for agentic engineering deserved attention.

In March, I saw mathematical verification becoming part of the answer to code quality in agentic engineering. Seven months later, the funding, research, and tools show why I was paying attention.

Axiom announced its $200 million Series A in March, extending its work in formal mathematics into verified AI. On October 22, Anthropic and Theorem published research proving specified security properties across 123 open-source libraries, under explicit assumptions.

Source: Anthropic, October 22, 2026. https://www.anthropic.com/research/formal-verification

My October 20 and 21 posts on verified AI and formal verification.

October 25, 2026 private conversation. Names and profile photos removed.

Formal verification is changing agentic engineering now. The interesting question is how that changes the work of building software.

Teams need evidence that AI-generated code meets their requirements

Every implementation an agent produces creates questions a team has to answer. Does this change preserve the behavior we depend on? Does it enforce the authorization rule? Can a retry execute the operation twice? Which inputs and execution conditions did we actually check?

Producing implementations faster increases the importance of answering those questions well. This is why I was paying attention in March. Formal verification gives us a way to establish specific properties of an implementation against a precise specification, within stated assumptions.

An agent can generate the code and construct a proof. A separate verifier checks the result. That changes the evidence a developer can ask for before accepting the work.

The specification feeds both proof construction and the verifier.

AI is reducing the work needed for formal verification

Formal methods have decades of work behind them. Researchers and engineers built the languages, proof systems, and techniques that make this moment possible.

AI is helping make the effort involved in applying those methods more accessible.

The funding and research matter for different reasons. Funding shows commitment to building in this direction. A checked proof establishes the particular property it covers. Adoption and maintenance experience tell us whether a workflow is useful to an engineering team. Each type of evidence answers a different engineering question.

Midspiral builds tools that connect AI coding workflows with external verifiers. I’ve talked with cofounder Fernanda Graciolli and met Holly Baker. Their coauthored paper, claimcheck: Measuring and Improving Specification Faithfulness, uses models to compare the meaning of a formal specification with the original requirement.

I discussed formal verification with Andrew Ng while filming my AI Code Review course at DeepLearning.AI. We disagreed about whether verification can run at the speed of code generation across a whole stack. That is a question I want engineering teams to test.

A proof only guarantees the property you asked it to prove

Imagine asking an agent to implement a money transfer. You specify that the total balance across two accounts must remain constant. The agent produces an implementation and a proof of that property.

Now ask three more questions. Did the sender authorize the transfer? Must the amount be positive? If a request is retried, can the transfer happen twice?

Preserving the total balance does not settle those requirements. Each needs to be addressed. A proof gives us a guarantee about the claim being checked. Deciding whether that claim captures the actual business requirement still takes engineering judgment.

This changes the review conversation. Teams can examine explicit guarantees alongside implementation details. They can ask what was proved, which assumptions it relies on, and what remains outside its scope. That is already a meaningful change in how we evaluate agent-written code.

Each row preserves the total balance. Authorization and retry checks catch different failures.

Clear software requirements matter more as AI writes more proofs

I knew mathematical verification would matter for agentic engineering in March. Here is my next prediction: as producing proofs becomes easier, specification quality becomes more valuable.

Teams need people and tools that help them express the right requirements, inspect proof coverage, and preserve guarantees as the software changes. I expect practical adoption to expand through selected components with requirements that can be stated precisely. One important property of one component is a useful place to start.

Then change the requirement. Change the implementation. See what maintaining the guarantee actually takes. That is the experience I want to see more teams publish: the property they proved, the assumptions they accepted, and the work involved in keeping the proof useful.

The March conversation is dated. The research and tools are here. Formal verification is changing agentic engineering now. When your agent delivers its next implementation, which property will you ask it to prove?