Eight Green Formal Proofs Became Five Fileable Ones When I Audited the SystemVerilog Assertions

I watched a synthetic formal board report 8/8 PROVEN, then watched its own audit certify only 5/8 as TRUSTWORTHY. That reversal is the premise of Proof Firewall, our runnable demonstration of governance for AI-generated SystemVerilog assertions (SVA), and it changed the standard I want a green proof to meet before it reaches a tape-out sign-off review.

I built the board with fixture-authored “LLM-authored” properties on a synthetic arbiter, a two-stage pipeline, and a CDC crossing because the uncomfortable case deserves to be visible. An assertion can look perfectly respectable in a property ledger. A formal engine can return a green result. Yet the implication may never have had to do any work, or it may continue to pass after the relevant design behavior has been broken. I had been treating the word PROVEN as a destination. Building this demo forced me to treat it as the beginning of an evidence review.

The Proof Firewall demo does not replace a formal engine, ingest real RTL, or call a live LLM in its default path. It is deliberately smaller and more inspectable: a pure-Python explicit-state model checker evaluates a synthetic transition-system IR, then a governance gate checks antecedent reachability, mutation kills, and cone of influence (COI). The output is either a reason to file a signed demonstration certificate or a reason to hold the result for human review.

I started with the wrong kind of green

I remember the first version of the board feeling reassuring precisely because it was so clean. Eight properties, eight green badges, and a bare-flow view that made the work look finished. My early instinct was to make the demo explain that clean result better. I thought the engineering task was presentation: surface the proofs, show the assertions, make the dashboard easier to trust. The green result was real, but it was answering a smaller question than the one a reviewer needs to ask.

Then I put the same eight properties through the checks that a filing conversation actually invites. Did the antecedent ever become true? Would the assertion object if a relevant part of the design were changed? Does it constrain a meaningful COI? Those questions are less flattering than a green badge because they ask what the proof has earned, not merely what the solver returned.

I had to abandon the first framing of the build. A screen that showed 8/8 PROVEN was an accurate view of the bare-flow baseline, but it was incomplete as a sign-off story. After the firewall audit, the same fixed synthetic board has five TRUSTWORTHY results, one VACUOUS result, and two WEAK results. The remaining three are not relabelled as success. They are held with the evidence that explains why. A proof label and a filing decision are different artifacts.

I chose the word “governance” carefully here. The demo's deterministic checks make the filing decision reviewable. An optional SVA author may propose an assertion, but the model checker and policy gate determine the verdict. Agents advise, code decides. I was trying to make the gate legible enough that the negative result would be useful rather than merely embarrassing. A withheld result needs a reason a verification engineer can inspect, reproduce, and challenge.

ARB3 made the problem impossible to ignore

I found the clearest failure in ARB3, the synthetic arbiter property assert (g0 && g1) |-> (turn == 0). In the bare flow, it is green. When I opened its waveform and reachability evidence, the antecedent g0 && g1 was unreachable in that synthetic arbiter. The implication had been proven only in the narrow sense that it was never forced to answer for the state it described. The antecedent never fires.

That distinction is easy to say and hard to keep present when a verification dashboard is full of green. I initially read the implication as a claim about arbitration behavior. The reachability result changed what I was looking at. It was a claim whose triggering condition never occurred. Calling that VACUOUS is more useful than preserving a green label, because it directs the reviewer toward the assumption or stimulus that made the proof empty.

I kept returning to this panel while working on the policy labels. VACUOUS can sound like a harsh result until the alternative is considered. If a sign-off record retains a proof without recording that its antecedent never fires, the review has received a conclusion without the condition that gives it meaning. The better record is the one that makes the limitation explicit and leaves a person something concrete to interrogate. That reachability record belongs beside the verdict.

I also had to resist treating vacuity as a cosmetic warning. If the property is meant to constrain an arbitration condition, unreachable triggering behavior is central evidence about whether the property exercised the intended behavior. The dashboard should not ask a reviewer to infer that from a green result. It should preserve the reachability finding, route the result out of the certificate path, and make the next review action obvious.

The industry context sharpened the stakes for me. The 2024 Wilson Research Group / Siemens EDA study cited in the demo specification reports 14% first-silicon success. That is not a Veriprajna measurement, and this synthetic board does not claim to explain that figure. It does make me less willing to treat a pleasant dashboard state as evidence by itself.

The pipeline property survived the breakage I expected it to catch

I hit the second failure while testing PIPE3, a synthetic two-stage pipeline property: assert v2 |-> (s2 == s2). I had wanted a concise example of an assertion that read sensibly enough to slide through a superficial review. The consequent is a tautology. It says s2 equals itself. The consequent constrains nothing.

The important move in the demo is not merely spotting the tautology in prose. The governance gate injects relevant single-point design mutations and asks whether the property kills them. For the featured weak pipeline case, PIPE3 records a 0/6 mutation kill result. The property survives the relevant broken variants. That is why the policy assigns WEAK rather than allowing the bare PROVEN result to stand as filing evidence. The mutation result tests useful sensitivity.

I learned something uncomfortable from trying to make this example feel less obvious. A human can read s2 == s2 and dismiss it quickly. Many weaknesses will not announce themselves so plainly. That is why I did not want the demo to depend on the operator spotting a suspicious string. The useful artifact is the procedure: reachability, a relevant mutation kill-test, COI, and a policy decision that records its reason.

I came to see the mutation check as a disciplined way of refusing a too-convenient reading of a proof. The goal is not to manufacture a dramatic failure. It is to ask whether the property would notice a relevant local change in the behavior it is supposed to constrain. When it does not, the result tells a reviewer something actionable: this assertion needs strengthening or a different review path before it can support the sign-off record.

This is also why the demo's benchmark needs a narrow description. Its local python -m backend.bench run scores 18/18 against a fixed labeled synthetic assertion set and identifies 6 proofs that the demo's own ungated baseline would have rubber-stamped. Those figures are a reproducibility check on this demo's labeled fixtures. They are not a production rate, a claim about AI-authored assertions generally, or a comparison with commercial formal tools.

I stopped trying to make the gate look permissive

I had a design choice after the first audit results: soften the withheld verdicts so the board felt more optimistic, or let the board decline to certify what it could not defend. I chose the latter because a real sign-off review needs the ability to distinguish a complete proof from a bounded one, an unreachable antecedent from a meaningful property, and a weak check from one that reacts to relevant broken behavior. Withholding is a review outcome, not a dead end.

That choice shows up in the policy vocabulary. TRUSTWORTHY earns the signed demonstration certificate. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD, and VIOLATED preserve different reasons for withholding that certificate or escalating the result. In the CDC fixture, for example, the stronger property assert (req && !ack) |-> ##1 req is VIOLATED and produces a concrete synthetic counterexample waveform. It illustrates a lost-transaction or CDC failure class. It says nothing about a customer chip.

I do not see this as a pitch for replacing a verification team's existing engine. The production direction is engine-agnostic: place a gate around an existing formal workflow, then make its acceptance criteria inspectable. Real-engine adapters and RTL ingest are deferred in this demo. The demonstrated boundary is intentionally narrow. That boundary matters because it keeps the claim proportional to what is actually running.

I now want the receipt beside the verdict

I keep thinking about the artifact a sign-off meeting needs when the assertion author is assisted by AI. It is not a confidence score from the author. It is a record that says which checks ran, what the reachability result was, which mutations were killed, what the COI contained, and why the policy permitted or withheld certification. The review needs evidence it can reopen.

That is what the demo exports in signoff_certificate.json: per-property verdicts, reachability, mutation results, COI, counterexample records where applicable, and a SHA-256 field. I built the certificate as a demonstration record because a reviewer should be able to reconstruct the decision without accepting a green badge on faith. A certificate should preserve the path to its verdict.

And if you would rather see it than read me describe it, here is the whole thing running end to end.

I made the demo runnable so the 8/8-to-5/8 reversal can be inspected rather than repeated as a slogan. The result I take away from it is modest but durable: a proof worth filing carries evidence of what it constrained, what it survived, and why someone may rely on it. Green remains useful. It simply needs a record that lets the next reviewer decide whether it deserves to travel further.