Verification Agents: What to Hand Over First, and What Keeps Them Honest

The 2024 Wilson Research Group study put first-silicon success at 14% of projects, the lowest level in two decades, so the appeal of agents in verification is easy to see. The published evidence is more mixed than the demos. In one preprint, the same agent flow and model lifted formal coverage by about 22 points on one design and about 8 on another. In another, assertions that compile and prove caught few injected bugs in a typical run.

So the useful question is the order of handover. This post sets out five stages, from work where an agent can do little damage to work it should only ever propose, and names the check that has to sit behind each one. A small worked example with illustrative numbers shows the sums: a triage agent that is wrong one time in ten saves 60 of 100 review hours, and one that is wrong 40% of the time saves nothing.

Key takeaways

• Hand over first the work whose result a deterministic tool or a quick human check can settle, and whose mistakes are cheap to undo.
• Proof, coverage and tool acceptance each have blind spots. A weak or vacuous assertion can still prove, and coverage can rise while the checkers stay weak.
• In the AssertLLM2 preprint, syntax success reached 95.00%, while the average bug kill ratio for a single run stayed between 5.08% and 11.69%.
• In our illustrative example, review still pays at a 35% wrong rate, though only just. Removing review altogether stops paying once more than 0.125% of auto-closed failures are wrong.
• Waivers, formal assumptions and sign-off stay with named engineers at every stage.

A test for what goes first

Ask four questions of any candidate task:

1. Can something other than the agent settle the answer? A simulator, a formal engine or a database lookup should be able to confirm or reject the output.
2. Is a mistake reversible? A wrongly routed failure costs an hour. A wrongly waived coverage hole can reach silicon.
3. Is checking much cheaper than doing? If review takes as long as the task, the agent has only moved the work.
4. Is the agent's evidence independent of what it is judging? Checks derived from the RTL under test can inherit the bug they should catch.

What each safety net does not catch

Each of the three common nets covers a different failure, and each has a gap.

Net	What it establishes	What gets through	What to add
Formal proof	The RTL satisfies the assertion under the stated assumptions	Vacuous or weak assertions, over-constrained environments, wrong readings of the spec, bounded or inconclusive runs	Vacuity and cover checks, mutation testing, review of every assumption
Coverage closure	Stimulus or proofs reached these parts of the design	Code that was exercised but never checked	Trace coverage points to checkers, and allow no agent-written exclusions
Review gates	A person accepted the change	Fatigue when volume rises, and agreement with a plausible explanation	Limit batch size, show the evidence with the change, and sample what was auto-approved

A 2026 University of South Florida survey of LLM-based verification, an arXiv preprint, draws the same line. Formal proof shows consistency with the implementation under analysis, not necessarily with the specification, and a passing tool run does not establish correctness. Our introduction to formal verification and its sign-off steps covers vacuity and over-constraint if you want the background.

The numbers show why the extra layers matter. AssertLLM2, an HKUST preprint from May 2026, tested models on 83 real designs and scored assertions against injected bugs. Syntax success reached 95.00% and leading models passed 60% on cone-of-influence coverage. Average proof coverage peaked at 23.30%, and the average bug kill ratio in its summary table peaked at 11.69%. Merging three runs lifted the best kill ratio to 18.51%. A dashboard showing only syntax and proof status would look far healthier than that.

The roadmap in five stages

The order and promotion tests below are our recommendation, not an industry standard, and your own data should move them.

Stage	The agent may	The net behind it	Promote when
1. Measure	Read logs and reports, and draft summaries nobody acts on yet	Shadow comparison with engineers' own conclusions	You have a baseline for triage time and a measured wrong rate
2. Regression housekeeping and triage	Select and launch tests, group failures, propose an owner	Deterministic promotion gates, and an owner can reassign	Wrong rate sits well below your break-even
3. Counterexample debug and assertion drafts	Propose root causes, fixes and new assertions	Formal rerun, vacuity and mutation checks, designer approval	Merged assertions kill mutants your existing set misses
4. Coverage closure	Add tests and properties for uncovered items	Additions only, new checks required, no exclusions	Added coverage comes with added checking, and later bugs show it
5. Planning and block-level runs	Draft plans and run the earlier stages in sequence	Approval at each plan step, traceability to the spec	This is the current ceiling, with sign-off still held by people

Stage 2: start with the plumbing

The most instructive example here is modest. A Samsung team's DVCon US 2026 paper, "A 3-tiered agentic AI Framework for Verification Regression", looked at 33 blocks before a first chip-level regression. Of 20,766 block-level tests, 2,892 had no recorded result, or 13.93%, largely through registration oversights and omitted options. The authors put the manual effort to find and rerun affected tests after a design change at two to three days.

Their agents watch releases, launch block-scoped runs, classify failures and route them to owners. The important part is that promotion to chip level is a plain threshold on block pass rate. In their trial, two blocks were promoted at about 91.2% and 83.1%, against an effective 23.6% in an earlier flow without the gate. The authors also say large-scale quantitative evaluation is still in progress, so this is early evidence. The pattern is worth copying: the agent does the chasing, and a rule makes the decision.

Stage 3: propose, and let the tool answer

Counterexample debug suits agents because the formal tool can check the result. FVDebug, from NVIDIA and presented at DVCon US 2026, was evaluated on a benchmark of 38 debugging challenges. A proposed fix counted as a pass if the original assertion passed when formal was rerun. It reports 71.1% at the first attempt and 86.8% within five attempts. A passing rerun is still weaker than a correct fix, because a change can silence an assertion without restoring the intended behaviour. A designer should approve every fix.

Assertion writing needs a longer chain, because a proof says less about whether the assertion was worth writing. Mutation testing is the most promising filter. An Edinburgh preprint from June 2026, "Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification", refines assertions until they kill injected faults, and reports six of seven designs finishing between 90% and 100% effective kill rate. The seventh, an SDRAM controller, stopped at 36.8% because some timing mutations produce no visible failure within the proof depth. So a surviving mutant calls for a look, and it does not always mean a weak check.

Two habits help here. Generate from the specification wherever possible, since the RTL under test may carry the bug. And cap the retries: Saarthi, an Infineon formal flow described in a 2025 preprint, hands over to a person after five failed iterations of a generate and update loop.

Stage 4: coverage, with additions only

Coverage closure looks like the obvious first job, because the target is a number. It sits this late because the number is easy to raise without adding protection. An Infineon and NIT Jalandhar preprint, "Agentic AI-based Coverage Closure for Formal Verification" from March 2026, added coverage agents to the Saarthi flow. With GPT-5, formal coverage on an ECC block rose from 70.30% to 92.11%, and on AXI4-Lite from 45.85% to 53.59%. On an automotive block, coverage rose from 72.67% to 79.05% while the proven rate fell from 62.22% to 51.68%. The authors point to harder properties, imperfect RTL extraction and some incorrect or duplicate properties, and those runs had no human review. More properties does not automatically mean more proof.

Simulation shows a similar wall. In AgentDV, a Clemson and Shandong preprint from August 2026, all three models tested stayed near 37% line coverage on an AES block despite branch coverage above 93%. Register-level tests could not drive the full sequence of loading a key and plaintext, starting the engine and reading the result. Datapath behaviour needed protocol knowledge and reference models the flow did not yet have.

Vendor results point higher, and they are claims. Synopsys, in a blog post dated 10 September 2026 about its DAC demonstrations, says its DV agent improved functional coverage by 12% and code coverage by 26% on an IP of about 12,000 lines, reaching more than 95% total coverage with a 50X productivity gain. We found no independent replication, so ask to run it on your own block.

The rule we would apply at this stage is simple. An agent may add tests and properties. It may not add exclusions, waive a hole or relax a constraint, and every addition aimed at functional coverage should arrive with a check that can fail.

Stage 5: planning, with approval at each step

A plan error spreads into everything built on it, so this comes last even though it comes first in the project. Our older note on what an effective verification plan should cover is a useful checklist for reviewing what an agent drafts. Siemens' press release of 27 February 2026 on the Questa One Agentic Toolkit describes a planning agent with engineers reviewing and approving each step, available through early access, and it publishes no performance figures. That approval model is the right default.

Our SoC lifecycle on The Semiconductor Hub shows the full-chip verification stage and its sign-off gate, which is where a named person should remain accountable.

A worked example: time saved against false positives

Every number in it is an illustrative assumption, not a measurement from any team or tool. Replace them with your own baseline from Stage 1.

Assumption	Value
Regression failures to triage each week	200
Manual triage per failure	30 minutes (0.5 hours)
Checking one agent proposal	6 minutes (0.1 hours)
Extra time lost following a wrong proposal, before triaging it manually	30 minutes (0.5 hours)

Without the agent, the week costs 200 × 0.5 = 100 hours. With it, every failure costs the check, and a wrong proposal adds the misdirection and the manual triage. If p is the wrong rate, hours per failure are 0.1 + p × (0.5 + 0.5), which is 0.1 + p.

Wrong rate (p)	Hours per failure	Hours per week	Saved against 100 hours
10%	0.20	40	60
20%	0.30	60	40
35%	0.45	90	10
40%	0.50	100	0
50%	0.60	120	Loses 20

Break-even is where 0.1 + p = 0.5, so p = 40%. For a sense of scale, MARVEL, an NYU preprint on agents for hardware security, classed 18 of its 51 reported issues as hallucinated, or 35.3%, on a known buggy SoC. That is a different task from failure triage, so it does not transfer directly, but at that rate this example would save only 10 hours.

The second sum is about taking the reviewer out. Suppose the agent auto-closes a failure as a duplicate of a known issue with no check. That saves 0.1 hours each time. If a wrongly closed failure hides a real bug that costs 80 hours to find later (also illustrative), then break-even is 0.1 ÷ 80 = 0.00125, or 0.125%, about one wrong closure in 800.

At 100 auto-closures a week and a 1% error rate, you save 10 hours of checking and incur one escape worth 80 hours. So the review gate is cheap insurance, and it should only come off where sampling has measured an error rate near that level. Compute costs sit on top of all this and grow with use, a theme of our post on the hidden cost of agentic AI.

What stays with people

• Formal assumptions and constraints. One wrong assumption can empty a whole set of proofs, and they will still pass.
• Waivers and coverage exclusions. These are risk decisions that someone must be able to explain later.
• Spec ambiguity. When the spec is silent, the agent should ask the architect rather than pick a reading.
• Sign-off. An agent can assemble evidence, and a named engineer accepts it.

Questions for any vendor or internal team

1. What was the wrong rate on a design the tool had not seen, and who classified the errors?
2. Do coverage gains come with new checkers, and how many mutants do those checkers kill?
3. Can the agent change constraints, assumptions or exclusions? Is that logged and blocked by default?

Sources

• Siemens EDA and Wilson Research Group (H. Foster), "IC/ASIC Functional Verification Trend Report - 2024", Verification Academy page dated February 2025.
• Wu et al. (HKUST), "AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications", arXiv:2605.27472, preprint, May 2026.
• Zheng et al. (University of South Florida), "A Survey on LLM-Integrated Hardware Design Verification", arXiv:2610.10580, preprint, October 2026.
• Choi, Noh, Yim and Kim (Samsung), "A 3-tiered agentic AI Framework for Verification Regression", DVCon US 2026 paper.
• Bai et al. (NVIDIA), "FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures", DVCon US 2026 paper.
• Krishnamurthy, Chitnis and Prodromakis (University of Edinburgh), "Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification", arXiv:2606.21451, preprint, June 2026.
• Kumar et al. (Infineon), "Saarthi: The First AI Formal Verification Engineer", arXiv:2502.16662, preprint, March 2025.
• Pothireddypalli et al. (Infineon, NIT Jalandhar), "Agentic AI-based Coverage Closure for Formal Verification", arXiv:2603.03147, preprint, March 2026.
• Goli et al. (Clemson, Shandong), "AgentDV: Closed-Loop Agentic AI for Hardware Design Verification", arXiv:2608.27148, preprint, August 2026.
• Collini et al. (NYU), "MARVEL: Multi-Agent RTL Vulnerability Extraction using Large Language Models", arXiv:2505.11963v3, preprint, February 2026.
• Synopsys (A. Thiruvengadam), "Agentic AI Drives Verification Closure and Thermal Analysis", blog post, 10 September 2026. Vendor claims.
• Siemens, "Siemens accelerates integrated circuit design and verification with agentic AI in Questa One", press release, 27 February 2026. Vendor statement.

The worked example uses illustrative numbers, and the stage order is our recommendation. Preprints may not be peer reviewed, and vendor figures are the companies' own claims. Some benchmarks cited tested Anthropic's Claude models, and the AssertLLM2 peak single-run bug kill and proof coverage figures quoted here are Claude's. This post was drafted with Claude, an AI model made by Anthropic.