Formal methods are genuinely great. Done right, they give you hardware that does not betray you and code that provably does what it says it does. But there is a catch, and it is a big one. The proof is only as good as your specification. You can verify a system to mathematical perfection against a spec that is two lines long, and the certificate will be worth exactly two lines of comfort. The genie grants precisely what you wish for. Nothing more. Nobody ever said the genie was on your side.

So the real problem was never the proving. Machines got good at that a while ago. The real problem is the wishing: taking messy, ambiguous, contradictory human intent and turning it into formal specifications that survive contact with real world systems. People have been chipping away at this for decades, with controlled natural languages, spec templates, and armies of very patient PhD students. Progress was real. It was also slow enough that most of the industry decided to just ship and pray.

Then LLMs got good, and a new family of techniques emerged, sometimes called neurosymbolic approaches to natural language formalization. The idea is simple to state and hard to do: take a natural language document, a policy, a requirement, a contract, and convert it into formal logic using LLMs and other AI powered tooling. The approaches vary. Some are interactive, keeping a human in the loop while the spec takes shape. Some are fully automated. Some build on Lean. Others, like AWS's Automated Reasoning checks, sit on top of SMT solvers.

Our own work at ICME builds on this foundation and pushes it further: succinct end-to-end proofs that the conversion, the battle testing, and the sign-off of a policy are carried along and defended across every agent action. We call it Proof-Carrying-Intent, and we will get back to it shortly. First, let's look at the state of the art in neurosymbolic formal methods, and be honest about what actually works.

What is the state of the art?

Like many fast moving fields this will not age well. But in summer 2026, where are we now?

The short answer: there is no single field here. There are at least four tribes working the same problem from different directions, and they mostly do not talk to each other.

But before touring the tribes, it is worth asking why they all ended up with the same architecture. Because they did. Every system in this post, from the math provers to the shipping products, is built the same way: a neural network that translates, bolted to a symbolic engine that decides.

Why everyone builds the genie the same way

The neurosymbolic literature splits the design space in two. The integrative approach puts the logic inside the network itself, building neural architectures out of differentiable logic gates so the reasoning is baked into the weights. The hybrid approach keeps the network and the logic separate: the LLM translates natural language into formal statements, and an external symbolic solver does the actual deducing.

A recent comparative study at NeSy 2025 built a best-in-class representative of each and concluded the hybrid approach wins, for two reasons that matter to everything below. First, integrative interpretability collapses at scale. You can read a network of five logic gates. You cannot read a network of 640 of them; at that point, the study notes, its interpretability is no different from an LLM's. Second, replacing the transformer with a logic architecture throws away everything the LLM was good at: the knowledge, the generalization, the ability to handle language nobody pre-formalized. The hybrid approach keeps the transformer for what transformers do and hands the logic to a solver that cannot hallucinate.

The same study surfaced a finding that should sound familiar by now. When they classified where their hybrid system failed, the syntactic errors, malformed logic the solver rejects, were nearly eliminated by constraining the LLM's generation to the solver's grammar, dropping the error rate from 17.8% to 1.5%. A constrained 7B model edged out an unconstrained GPT-4. What remained were the semantic errors: logical forms that parse perfectly and mean the wrong thing. One premise says "1519," another says "16th century," and the solver, doing flawless deduction over an unfaithful translation, gets the right answer to the wrong question.

Hold onto that distinction. The syntax problem is an engineering problem, and the field has largely engineered it away.

Now, the tribes.

The mathematicians got there first

The flashiest progress is in formal math. AlphaProof and AlphaGeometry hit silver-medal-level performance on IMO 2024 problems, and by 2025, ByteDance's Seed-Prover achieved a gold-medal IMO score with formal solutions, alongside Harmonic's Aristotle. Math Inc.'s Gauss autoformalization agent has been formalizing real research mathematics in Lean, including completing a challenge set by Terence Tao and Alex Kontorovich to formalize the strong Prime Number Theorem. Open source is not far behind, with DeepSeek-Prover-V2, Kimina-Prover, and Goedel-Prover-V2 posting strong results on standard benchmarks like MiniF2F and PutnamBench.

Here is the fine print, though. Even AlphaProof's silver-medal run required humans to manually translate the problem statements into formal language before the machine took over. The proving is superhuman. The wishing is still artisanal. And the benchmarks tell on themselves: fine-tuned autoformalizers hit 96% on MiniF2F but drop to around 16% on college-level problems, exposing how starved the field is for natural-language-to-formal-language training data. The genie aces the exam it studied for.

The temporal logic crowd

The second tribe cares less about theorems and more about behavior over time: robots, hardware, requirements documents. The tooling here is a whole family tree now. NL2LTL converts natural language instructions to linear temporal logic, NL2TL and Lang2LTL translate natural language commands for robotics, and nl2spec interactively translates unstructured natural language to temporal logics. The nl2spec approach is worth pausing on because it takes ambiguity seriously: it maps subformulas of the formalization back to fragments of the original sentence, so a human can add, edit, and delete sub-translations instead of wrestling with the entire formalization at once. That is the interactive philosophy in one line. Do not pretend the ambiguity is not there. Surface it, and make the human resolve it.

The newer work is trying to put guarantees on the translation step itself, which is where this gets genuinely interesting. Grammar-forced translation of natural language to temporal logic landed at ICML 2025, and ConformalNL2LTL translates natural language instructions into temporal logic formulas with conformal correctness guarantees. Read that again. Statistical guarantees on the wish itself. Not a solved problem, but the right problem.

Shipping it

Then there is AWS, whose automated reasoning group did the hardest thing of all: made this work at production scale for people who have never heard of an SMT solver. Automated Reasoning checks in Bedrock Guardrails let you upload a source document, an HR handbook, a compliance manual, a product spec, and the system extracts formal logic rules and a variable schema, translating natural language into logic that can be mathematically verified. Under the hood it is real formal methods, not marketing: rules are expressed in a subset of SMT-LIB syntax, mostly as if-then implications.

Two design decisions here are genuinely ahead of the field. First, they measure the wish. Every policy gets a fidelity report with a coverage score, how much of the source document made it into the policy, and an accuracy score, how faithfully the rules represent the source. That is a direct, quantified answer to "is my spec two lines long," and almost nobody else offers one. Second, they treat translation uncertainty as a first-class citizen. Multiple LLMs independently translate the natural language, and the system only returns findings where a significant percentage of them agree; when they cannot agree, the result is TRANSLATION_AMBIGUOUS rather than a confident wrong answer. That kind of epistemic honesty is rare in a product. AWS reports up to 99% accuracy at detecting correct responses, and their testing workflow generates scenarios that surface gaps in your written policy before they surface in production, the "wait, did we really mean to allow that" moments. This is the genie asking clarifying questions before granting, and it is exactly the direction the whole field should be heading.

The safety people

The fourth tribe is playing the longest game. ARIA's Safeguarded AI programme, led by David "davidad" Dalrymple, aims to build a "gatekeeper" AI that ensures other AI agents only operate within agreed-upon guardrails, combining scientific world models with mathematical proofs to get the kind of safety assurances we expect from nuclear power and passenger aviation. The programme's ambition is an open-source mathematical assurance toolkit that lets fleets of AI agents produce formally verified artifacts at speed and scale, and in early 2026 it pivoted its deployment focus toward cybersecurity applications. When a £59m moonshot narrows its aim, pay attention to where it narrowed to. High-assurance cyber defence is where they think the proofs meet reality first.

And the academic edge of this tribe is starting to verify the cage rather than the animal. A recent containment verification line of work formally verifies the agentic framework itself, the conventional software that mediates every action an LLM agent takes, proving boundary-event safety for every typed action the AI can emit, independent of the AI's capability or strategy. The formal artifacts are synthesized by an LLM pipeline in Dafny, with an architectural information barrier that rules out tautological specifications by construction. You may not be able to prove what the model is thinking. You can prove what it is allowed to do.

The honest scoreboard

So that is summer 2026. The provers are gold medalists. The translators are getting confidence scores and conformal guarantees. The teams shipping to production are pairing SMT-backed policy checks with fidelity reports. The safety people are verifying the guardrails instead of the model.

What nobody has fully solved is the thing this post opened with. Every one of these systems still has a translation step where meaning can leak, and the leak is specifically semantic: grammar constraints and syntax checkers can guarantee the formal output parses, but nothing yet guarantees it means what the sentence meant. Evaluating whether a formalization actually aligns with the informal statement has mostly depended on manual verification and human battle-testing, which is exactly the labor-intensive bottleneck the field is racing to automate. The wish still has to be checked and signed off by someone. Which brings us to what we are building.

Where ICME fits: check the wish before the genie moves

Everything above shares a quiet assumption: the thing being verified sits still. A theorem, a document, a chatbot answer. But agents do not sit still. They send emails, move money, delete files, sign up for things. An agent's mistakes are not wrong answers you can regenerate. They are actions, and actions do not have an undo button.

That is the gap ICME PreFlight lives in. You write your policy in plain English. Never send funds to an unverified wallet. No transaction over 10,000 USD without a second confirmation. PreFlight compiles it into SMT-LIB formal logic once, the same hybrid neurosymbolic architecture running through this whole post: language models do the translation, symbolic solvers do the deciding, and each half covers the other's weakness.

But compiling the wish is not the same as getting the wish right, and this is where the genie metaphor stops being a joke and becomes a product feature. A policy can compile cleanly and still mean something you did not intend. So before your policy touches a single real action, PreFlight battle tests it: it generates adversarial scenarios, combinations of variable assignments that are logically possible under your rules as written, and surfaces the most suspicious ones first. You review each one and answer a single question: could this actually happen in my domain? Thumbs up becomes a test case. Thumbs down becomes an annotation, and the policy gets rebuilt to close the loophole. This is the genie reading your wish back to you, loopholes highlighted, before anything gets granted. Your intent is not assumed to be captured. It is tested until you sign off.

Then, at runtime, the flow respects your agent's actual life. Most of what an agent does is harmless: reading files, formatting output, fetching URLs. In a typical session, 80 to 90 percent of actions never touch a policy variable, and running a full formal check on them would be waste. So every proposed action first passes through a free relevance screen that answers one fast question: does this action touch any variable in your policy? If not, the agent proceeds, no charge, no latency tax. If it does, the action gets the full treatment: three independent solvers, a local extraction model, an automated reasoning engine, and Z3, each evaluating the action separately, with consensus required before a verdict comes back. SAT, the action proceeds. UNSAT, it is blocked. Under a second, about a cent, and every check produces a cryptographic proof that the guardrail actually ran and actually returned that verdict, a receipt you can hand to any third party.

A few design decisions are worth stating plainly, because they encode a worldview. First, PreFlight fails closed: anything other than an explicit SAT, including timeouts, errors, and malformed responses, means the action does not happen. An agent that cannot reach its guardrail is an agent that does nothing, which is exactly what you want. Second, a blocked action is blocked. The agent does not get to rephrase the request and try again, because agents, like lawyers and toddlers, will absolutely try. Third, the enforcement mechanism is not a model. Prompt-based guardrails, LLM judges, and reasoning checks all share one weakness: they can be jailbroken, injected, and argued with, because the guardrail and the attack speak the same language. An SMT solver does not speak that language. When PreFlight returns UNSAT, that is not a vibe, it is a mathematical statement that no interpretation of the action satisfies your rules, and there is no prompt that talks a solver out of arithmetic.

Proof-Carrying-Intent

Which brings us back to the promise from the top of this post.

Start with the trust gap the receipts above already close. Nearly every guardrail in this field runs on somebody's infrastructure and returns a verdict, and a verdict is not evidence. The counterparty on the other side of an agent transaction, the vendor, the payment processor, the regulator, has exactly two options: trust the operator's word that the guardrail ran, or re-run the entire pipeline themselves. Auditability is not verifiability. A log entry says a check happened. It does not prove it. This is why every PreFlight check ships with a cryptographic proof rather than a promise: the receipt, not the operator, is what the third party verifies.

But a per-action receipt certifies one action, against one policy, at one instant. And that is not how agents work anymore. Tell an agent "book my trip to Denver, spend at most 2,000 USD total and no more than 1,000 USD per day," and the job does not stay with one agent. An orchestrator decomposes it. One sub-agent finds flights, another books the hotel, a third arranges the ride from the airport.

Now watch the single-action check fail twice. It fails across agents: the sub-agents never saw your instruction, only whatever policy they were handed, and a clause dropped at any hand-off is invisible to every check downstream. A stack of individually valid receipts tells you nothing about whether the job as a whole carried your intent. And it fails across time: the flight agent spends 600 USD and its check passes. The hotel agent, which knows nothing about the flight, spends 550 USD and its check passes. Together they just blew your 1,000 USD daily cap, and no check ever saw both numbers. The daily cap was never a property of any single action. It was a property of the story, and single-shot checks do not read stories.

Proof-Carrying-Intent is our name for closing this gap. The idea has three moves. First, the wish gets read back before the genie does anything: your instruction is formalized into a machine-checkable predicate, battle tested against generated scenarios exactly as described above, and then signed by you. The signature makes it the authorized intent, fixed at the root before any agent acts. Second, that signed intent travels with the delegation. Every sub-agent's action is checked against it, together with the accumulated state, the running totals, that single-shot checks cannot see. The hotel agent's check arrives already knowing about the flight agent's 600 USD. Third, every check folds into the proof carried from the actions before it, so what comes out the far end is one short receipt certifying the whole delegation: every action was checked against the intent you signed, none violated it, cumulative clauses included, and anyone can verify it in milliseconds without trusting a single agent in the chain.

Two properties of that receipt are worth savoring. It can be demanded at any point, not just at the end; a counterparty mid-delegation can verify everything up to that moment. And disclosure is selective: the flight agent never learns your lodging budget, and a verifier can confirm your policy was enforced without learning anything about what the policy says. Your purchasing thresholds are your business. The proof that you enforced them is everyone's.

And in the spirit of this post, the honest fine print, stated up front because everyone else buries it. The proof attests that your signed wish was enforced, not that it was wise; if you sign a bad policy, you get cryptographic certainty that your bad policy was followed to the letter, which is the genie's oldest trick. This is exactly the risk battle testing exists to shrink: the adversarial scenarios are the loopholes in your policy shown to you before you sign, so the wish you authorize has already survived an attempt to abuse it. We think there is much more to do here, and we have additional methods for hardening the wish itself.

We have research in review on all of this, so the full details will have to wait. But the destination should be clear from everything above. The field spent the last few years teaching machines to formalize our wishes. Next up is proving the wishes were honored, across every agent, every action, and every hand-off in between.

The wish, the grant, and a receipt. For the whole story this time, not just one scene.