Rethinking Formal Verification in the AI Era

By Kanav Arora, ML Researcher at ChipAgents

Most hardware teams already understand why formal verification matters. It can expose corner cases that simulation may never reach and establish critical behaviors across the modeled state space.

The unresolved question is not whether formal works. It is why formal remains a specialist intervention instead of becoming a repeatable part of verification wherever it could materially change a project outcome.

Recent advances in AI and automation suggest an obvious answer: make assertions cheaper to write, assemble testbenches faster, and launch more proofs. All of that is useful. But it locates the bottleneck at the most visible part of the work.

A property can be precise and still encode the wrong contract. A regression can be green and still fall short of sign-off. Before a useful property can be written, someone has to decide what the design is responsible for, at which boundary, and under which assumptions. After the solver returns, someone has to decide what the result means and whether the evidence is strong enough to rely on.

The harder question is therefore not simply, “Can we prove this property?” It is:

What exactly should be verified, under which assumptions, and what would be enough to sign it off?

Formal verification is not only a property-generation or proof-execution workflow. It is the engineering discipline that connects design intent to defensible evidence. The proof is only the middle.

The Work Before the Property

Formal is rarely applied at the same level at which a feature is described. A requirement may be written at the SoC or subsystem level, while the proof runs at a module or submodule boundary. The formal engineer has to translate an end-to-end behavior into obligations that are observable and provable at that smaller boundary.

Consider a requirement that every accepted request eventually produces the correct response. At a module boundary, that sentence immediately branches into questions. What counts as acceptance? Can backpressure delay the response indefinitely, or is eventual readiness an explicit promise about the environment? If it is an assumption, which adjacent block is responsible for guaranteeing it? Does a flush cancel an accepted request or preserve it? What happens across reset? Which ordering guarantees belong to this module?

Each answer changes the assertions, assumptions, covers, and reference model. The assertion syntax is not the difficult part. The difficult part is recovering the contract.

That contract is rarely contained in one document. Relevant intent may be distributed across the main specification, feature documents, protocol definitions, architecture diagrams, design reviews, simulation environments, previous checkers, and explanations remembered only by designers. Those sources may disagree or describe only the common case. By the time formal work begins, important context may already have been compressed or lost.

RTL helps, but RTL is evidence, not automatically intent. It reveals the implemented hierarchy, state, interfaces, and candidate corner cases. It cannot, by itself, resolve what the implementation was supposed to do. If properties are derived only from RTL behavior, formal can prove that the design does what the design already does, including the bug.

A serious formal plan must therefore keep several kinds of evidence separate: behavior explicitly required by the specification, behavior implied by an architectural or interface contract, behavior visible only in the implementation, and behavior that remains genuinely ambiguous. Assertion generation can turn any of these into code. It cannot decide which of them is authoritative.

When the Specification Runs Out

Specifications are often incomplete precisely where formal demands a decision. Reset interactions may be absent. Backpressure may be described only for steady-state operation. An ordering guarantee may be assumed but never assigned to an owner. Error handling may have changed without the main document being updated.

Formal does not forgive vague intent. It forces ambiguity into the verification model: as a property, an assumption, an omitted scenario, or an unresolved choice. That pressure is useful because it exposes missing definitions, inconsistent timing, unowned obligations, and assumptions that no component actually guarantees.

An Intel case study makes the effect unusually concrete. In its coverage-driven formal sign-off methodology, formal work led the team to clarify or improve 78 of 104 requirements for a micro-sequencer. The verification effort was improving the specification and architecture, not merely checking an already-complete document.

When intent is missing, the answer is not to infer it silently from RTL or let an AI system select the most plausible interpretation. Formal can make competing interpretations executable, showing how each changes the local contract and its reachable behaviors. The unresolved decision then returns to the designer or architect who owns it. The output is a reviewed contract with a source, an owner, and a visible effect on the verification plan, not a confident guess buried in a checker.

The Environment Is Part of the Claim

A proven property is powerful, but precise: the modeled design satisfies the property under the supplied assumptions. It does not establish that the property expressed the intended requirement, that the property set is complete, or that the environment preserved every legal behavior.

Suppose the response interface can stall. An assumption that the downstream block is always ready may make an eventual-response property easy to prove, while excluding the behavior most likely to expose a dropped request or an unstable response. The proof is not mathematically false. It has answered a narrower question than the architecture required.

A weaker assumption that the downstream block will eventually become ready may be legitimate. But it is an architectural commitment, not a solver convenience. A neighboring block must guarantee it, a higher-level proof must establish it, or the system must accept it explicitly as an external constraint. Otherwise two blocks can each assume the behavior that the other was supposed to guarantee, leaving a circular argument that no local proof will expose.

A related failure mode is antecedent vacuity: a request-response assertion can pass because no request is ever accepted. The foundational work on vacuity detection by Beer, Ben-David, Eisner, and Rodeh showed why a valid temporal property can still conceal a real modeling or specification error: an implication may be true only because its precondition is unsatisfiable.

Assumptions and covers are therefore not testbench plumbing. They are part of the verification argument. Every assumption needs a justification at this boundary and evidence that it is guaranteed. Important scenarios need reachability evidence. If an accepted request followed by a stall and eventual response cannot be covered, a page of passing assertions may be describing the constraints rather than the design. But an unreachable cover is evidence to investigate, not proof of overconstraint; the cause may instead be dead behavior, an incorrect cover or reset model, or insufficient exploration.

A Green Regression Is Not Sign-Off

Assertion count and pass rate are useful project telemetry, but neither is a standalone closure criterion.

A count has no denominator. Ten overlapping properties can inflate it; one carefully chosen end-to-end checker can carry more verification intent than a hundred local invariants. A pass rate says how the properties performed, not whether the missing behaviors were ever turned into properties.

The Intel study offers a useful warning. The authors report that proving the requirements-derived assertion set, with roughly 5 percent of the properties still bounded, had exposed 80 percent of the design bugs eventually found. Coverage closure exposed the remaining 20 percent by revealing unexpected overconstraints and missing assertions associated with missing requirements. The green results were real. They were not the entire sign-off case.

This is the difference between a proof result and formal closure. A result tells us how a stated obligation behaved under a modeled environment. Closure is the argument that the project stated the right obligations, preserved the right behavior, and obtained evidence strong enough to rely on.

What Sign-Off Must Establish

A 2016 live case study of formal sign-off organizes closure around three questions: Is the end-to-end checker set complete? Have unintended overconstraints been removed? Has every checker reached a justified proof depth? Those questions are more useful than a single coverage percentage because each exposes a different way for a green result to mislead.

The first question, checker completeness, is also the hardest. It begins with traceability from requirements to boundary-level obligations, but traceability alone shows only that a link exists. The property set must also be capable of observing the design behavior that matters.

Coverage Models for Formal Verification describes several ways to examine that problem. In one testbench considered fairly complete, 5,423 assertions still left 18 percent of the design’s registers outside every assertion’s cone of influence. For the running example, the corresponding question is concrete: does any property even reach the response-hold and backpressure logic? The number of assertions was large; the unobserved logic was larger than the dashboard implied.

Cone-of-influence coverage asks which RTL elements could affect the property suite; it is a structural scope measure, not evidence that a proof depended on all of that logic. Proof-core analysis asks which subset was sufficient for a particular proof. Related, but not identical, research on Inductive Validity Cores and proof-based coverage formalizes proof-sufficient subsets of transition-system models, and more than one minimal core may exist. These methods can reveal insensitivity in a property set. They do not establish that the requirements themselves are correct.

Mutation-based qualification asks the same completeness question from the opposite direction: if selected behavior in the design were changed, would a previously passing property fail? Holger Busch’s industrial work on mutation coverage for formal property checking uses deliberately instrumented faults to test the sensitivity of a property set. Would dropping an accepted request or breaking response stability be detected? A surviving mutant is a question to investigate, not proof that a requirement is missing; a killed mutant shows sensitivity to that injected fault, not universal completeness. The result is only as strong as the chosen fault model.

The second sign-off question concerns the environment. Every useful formal environment excludes illegal behavior. The issue is not whether it is constrained, but whether every exclusion follows from an interface contract, another component’s guarantee, a higher-level proof, or an explicit system constraint. Stimuli coverage, reachability analysis, cover properties, and cross-checks against neighboring blocks provide different evidence that legal scenarios have not been removed for the sake of convergence.

The third question is what the tool actually established. An unbounded proof and a bounded result carry different information. In the methodology described by Kim and colleagues, a bounded result establishes that no counterexample exists through the explored depth from the modeled initial states and under the supplied assumptions; it is not an unbounded proof. But bounded does not mean worthless. Sign-off with Bounded Formal Verification Proofs describes how a required proof depth can be justified from latency, initialization, microarchitectural structures, targeted corner-case covers, formal coverage, and failures observed elsewhere.

The right question is therefore not whether every property is unbounded at any cost. It is whether every result has been qualified against the behavior it is meant to cover, and whether the remaining uncertainty is explicit. That qualification is property-specific: a depth justified for a bounded-latency response does not, by itself, establish an open-ended eventual-response claim.

No single metric establishes completeness. Requirement traceability, environment validation, proof-depth qualification, proof cores, and mutation coverage provide complementary evidence. Sign-off is the engineering judgment that the combined evidence is sufficient for the risk the project is carrying.

The Work After the Proof

Verification intent is not finalized when the first plan is written. Proof results change the team’s understanding of both the design and the verification problem.

A counterexample shows that the modeled design and environment can violate a property. It does not diagnose which artifact is wrong. In the request-response example, a trace in which an accepted request disappears after a flush could expose an RTL bug, a property that omitted the cancellation rule, or a specification that never decided whether the request survives.

Other outcomes are equally conditional. An unreachable cover may reveal an overconstrained environment or genuinely dead functionality. Non-convergence is not evidence that the design is wrong; the result has not been established with that model, boundary, and proof strategy. Even a successful proof can create work if vacuity or proof-core analysis raises a question about whether the obligation exercised and observed the intended behavior.

These outcomes should update the verification plan rather than remain in tool logs. New assumptions should be linked to their guarantees. Clarified requirements should be traced to affected checkers and covers. Coverage gaps should become questions, properties, or explicit waivers. Debug knowledge should survive to help the next block with the same protocol or failure pattern.

This is also where company-specific methodology matters. Experienced teams accumulate interface contracts, reference models, abstractions, helper invariants, checker patterns, waiver rules, and sign-off expectations. Those assets are reusable only when their context survives. A constraint copied without its original boundary can propagate an unsound assumption as efficiently as good engineering.

A Role Worth Testing for Automation

This suggests a plausible role for agents, not an established result. A useful agent-based system would aim at something narrower than “write more assertions,” but potentially more consequential.

It could maintain the chain around a proof: requirement to block-level obligation, obligation to property and assumption, and result to coverage and sign-off evidence. It could flag downstream artifacts invalidated by a specification change, expose unowned assumptions or conflicting interface rules, and carry a coverage gap back into the plan. This is continuity work that teams repeatedly reconstruct by hand.

What it cannot do is make intent authoritative by expressing it confidently. It should not resolve an undocumented flush rule from RTL alone, declare an assumption legal because it helps convergence, or turn a high assertion count into a sign-off claim. A system that converts uncertainty into polished assertions has automated the wrong thing.

The formal engineer and design owner still approve the contract, environment, abstractions, and evidence. The useful ambition is not to automate away that judgment. It is to give the judgment better context and prevent its reasoning from disappearing between documents, tools, teams, and project phases.

What Makes Formal Scale

The practical test is not how many assertions were generated or how many proof jobs are green. For an important behavior, can the team trace the requirement to a boundary-level obligation, show who guarantees every assumption, demonstrate that the scenario is reachable, explain the strength of the result, and say what changed because of proof?

If not, the dashboard is ahead of the verification.

Formal scales when the reasoning that surrounds a proof becomes as explicit and reviewable as the property itself. That means treating incomplete intent, environment contracts, proof depth, and coverage qualification as first-class engineering work, not overhead around assertion writing.

Sign-off must defend why the team chose the right obligations, under a legitimate environment, and why the evidence is sufficient. The solver returns an answer; the work around it determines whether that answer deserves our confidence.

Kanav Arora is a ML engineer and Formal Verification lead at ChipAgents, where he works at the intersection of agentic AI and semiconductor verification. He focuses on building autonomous systems that help engineers develop, run, and refine formal verification workflows, making FV more scalable and accessible across hardware teams. His work spans AI agent design, verification methodology, and developer tooling, with an emphasis on translating advances in AI into practical, reliable engineering workflows.

References

• Ang Li, Hao Chen, Jason K. Yu, Ee Loon Teoh, and Iswerya Prem Anand, “A Coverage-Driven Formal Methodology for Verification Sign-off”, DVCon 2019.
• Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh, “Efficient Detection of Vacuity in Temporal Model Checking”, Formal Methods in System Design, 2001.
• Ipshita Tripathi, Ankit Saxena, Anant Verma, and Prashant Aggarwal, “The Process and Proof for Formal Sign-off: A Live Case Study”, DVCon 2016.
• Xiushan Feng, Xiaolin Chen, and Abhishek Muchandikar, “Coverage Models for Formal Verification”, DVCon 2017.
• Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen, Mats P. E. Heimdahl, and Lucas Wagner, “Proof-Based Coverage Metrics for Formal Verification”, ASE 2017 (DOI).
• Holger Busch, “An Efficient Methodology for Mutation-Coverage-Collection of Formal-Property-Checking”, DVCon 2022.
• NamDo Kim, Junhyuk Park, HarGovind Singh, and Vigyan Singhal, “Sign-off with Bounded Formal Verification Proofs”, DVCon 2014.

Share this post via:

• 
• 
• 
•