Bharat Bhavnasi San Francisco, CA, USA

Verification Is Becoming the Agent's Substrate

• 5 min read
#agents #verification #security #planning #rl

The most useful agents shipping right now are not the ones with the cleverest prompts or the longest context windows. They are the ones whose output lands in a column a machine can check. Look at what crossed a capability threshold in the last two weeks — autonomous vulnerability discovery, verifiable planning, formal oversight — and the common thread is not a smarter model. It is that the work product became checkable, and the checker became the load-bearing component. If you are building agents and still treating verification as a post-hoc eval step, you have the architecture inverted.

Security agents are the proof of concept

The clearest signal came from Anthropic’s Project Glasswing, disclosed May 23. Inside its first month, the unreleased Claude Mythos model surfaced more than 10,000 high- and critical-severity findings across over a thousand open-source projects, including a CVSS 9.1 flaw in wolfSSL (CVE-2026-5194) that would have let an attacker forge certificates. Anthropic reports the model autonomously chained Linux kernel bugs from ordinary user access to full machine control.

It is not a coincidence that offensive security is where frontier agents matured first. Exploitation is the canonical verifiable task: a shell pops or it does not, a forged certificate validates or it does not, a privilege escalation lands or it crashes. There is no judge to argue with. That binary, executable ground truth is exactly the reward signal an agent can be trained against and exactly the filter that turns a flood of low-confidence guesses into 1,726 confirmed true positives. The disclosure is mostly read as a cybersecurity arms-race story, and it is. But the more durable lesson for builders is methodological: when your task has a cheap, mechanical oracle, agents scale to superhuman throughput. When it does not, they generate plausible noise.

That asymmetry is also the catch Anthropic flagged itself — finding flaws is now far cheaper than fixing them. The verifier scales the easy half of the loop and leaves the hard half to humans. Plan your roadmap around which half you are actually automating.

Planning is being recompiled into checkable artifacts

The same shift is reshaping the planning literature, which spent two years asking the wrong question. The ICAPS 2026 position paper Planning in the LLM Era (May 21) argues bluntly that using an LLM as the planner is “unsound and incomplete by its very nature” and burns compute without generalizing. The field’s realignment is to stop using the model as the planner and start using it as a compiler: at construction time the LLM emits a symbolic solver or plan representation, and at inference time a verifiable, deterministic engine runs it. The language model moves out of the hot path entirely.

This is the same instinct as FormalJudge, which decomposes an agent’s trajectory into atomic facts and discharges them through an SMT solver to produce an actual proof of correctness, and SymCode, which reframes math reasoning as verifiable SymPy code generation. Across planning, oversight, and reasoning, the pattern repeats: don’t trust the generation, trust a separate component that can mechanically check it. The LLM’s job is to propose; the verifier’s job is to dispose. Architecturally, that means your interesting design decisions are no longer about the agent loop — they are about what representation you ask the model to emit so that something cheap and deterministic can validate it.

The training signal is following the same gradient

Reinforcement learning has already internalized this. RL from verifiable rewards (RLVR) is now the default recipe for reasoning models precisely because it only awards credit when output passes a programmatic check — unit tests for code, exact-match for math, a working exploit for security. Agent-RLVR extends it to software-engineering agents by pairing environment rewards with guidance, and it works for the same reason Glasswing works: the environment is the verifier.

But this is also where the honest tension lives. As The Verifier Problem Nobody Has Solved lays out, RLVR’s success is confined almost entirely to domains where a cheap oracle already exists. Math, code, and exploitation have ground truth; legal reasoning, product strategy, writing, and most real knowledge work do not. The current frontier is not building a smarter agent — it is building a verifier for tasks that have never had one. Reward models, LLM judges, and reference-based rewards are all attempts to manufacture a checker where reality refuses to supply one, and all of them leak. Treating a learned judge as if it were an executable oracle is how you train an agent to game the judge.

What this means if you are building

The practical takeaway is a design discipline, not a framework. Before you wire up another agent loop, ask where your task sits on the verifiability axis. If a deterministic check exists — a test suite, a type checker, a SAT/SMT condition, a schema, a transaction that either commits or rolls back — make that check the spine of your system, push the LLM toward emitting artifacts that hit it, and reserve the model for proposal and repair. If no such check exists, your first and hardest engineering problem is constructing a proxy verifier, and you should be deeply skeptical of any throughput claim until you have one. The moat in mid-2026 is not the model. It is the verifier you can put behind it.

Worth bookmarking

Share:
Suggest changes