What's inside a reproducible proof bundle

“Formally verified” is a sentence. A proof bundle is a folder you can open. We just published one you can clone right now - github.com/VoskenAI/vosken-certified-samples, Apache-2.0, two RTL primitives with their complete formal proof bundles and a one-line certificate for each. This post is not the pitch. It is the unboxing: what is actually in the folder, why each file earns its place, and what happens when we run the proof against RTL we deliberately broke.

The problem

You have read “formally verified” on enough datasheets that the phrase has stopped meaning anything. The usual evidence is a PDF, a screenshot of a CI job you did not run, or a sentence with no artifact behind it. None of that is reproducible - reproducible means you re-run it, on your machine, and get the same answer. We wanted to stop describing that and just ship it.

Show the failure

Picture the report a lot of “verified” IP ships with: a summary paragraph, a green checkmark, no way to check either. Nothing in it can go red, because there is nothing in it you can run. It passes every review, and that is exactly when it should worry you - a claim that cannot fail is not a claim you have tested, it is one you have taken on faith.

Key Lesson: If a verification claim has no command attached, it is marketing wearing an engineering costume.

Why it fails

A real proof bundle has to answer three questions a summary cannot: what exactly was proven, against exactly which bits of RTL, using exactly which toolchain. Drop any one of the three and the claim stops being checkable - a proof with no RTL hash could describe a file that shipped separately; a proof with no pinned toolchain might not reproduce on a newer solver; a proof with no failure mode might never have explored a single interesting state. Each primitive in the published repo answers all three with one directory:

<primitive>/
├── rtl/          # the DUT, never modified by the proof
├── formal/       # the SymbiYosys config, properties, assumptions, covers
└── VERDICT.txt   # the certificate: hash-bound, tool-pinned, PASS/FAIL per assertion

Key Lesson: A proof bundle is not the proof plus documentation. It is three things that check each other - the RTL, the property set, and the certificate binding one to the other.

The fix, three files with real content behind each

formal/fv_wrr_arbiter.sby is the harness for the weighted round-robin arbiter. It names its own frontend choice for a reason worth keeping: native read_verilog silently drops the bind construct, so the properties would compile but never attach.

# Frontend: yosys-slang (read_slang) - the only open-source frontend that
# honours SystemVerilog bind. Native read_verilog silently drops bind.
[tasks]
prove
cover

[options]
prove: mode prove
prove: depth 12
cover: depth 28

[engines]
smtbmc z3

The properties themselves are ordinary SVA, asserted directly against the DUT’s signals - no indirection to hide behind:

// P_GNT_ONEHOT0: grant is one-hot-or-zero
always_comb begin : sec_grant_shape
    if (rst_n) begin
        P_GNT_ONEHOT0_A: assert ((gnt & (gnt - 1'b1)) == '0);
    end
end

// P_NO_STARVE: the wait count stays strictly below sum(weight)
// whenever a requester with positive weight is waiting.
always_comb begin : p_no_starve
    if (rst_n) begin
        P_NO_STARVE_A: assert (!(req_fidx && w_fidx_pos)
            || (f_wait_q < sum_w));
    end
end

VERDICT.txt is what ties the first two to a specific set of bits. It opens by naming exactly what it is binding:

# This certificate binds a formal verdict to exact RTL bits and an exact
# toolchain. reproduce.sh re-runs the proofs and diffs every line below.

[dut_md5]
43b5b2c044f3d828444f0931bea4ad80 rtl/wrr_arbiter.sv
8f82dcd1209895803a7be4bbc1f829e2 rtl/rr_arbiter_tree.sv

[prove]
PASS ASSERT u_n2.u_fv_wrr_arbiter.sec_grant_shape.P_GNT_ONEHOT0_A
PASS ASSERT u_n2.u_fv_wrr_arbiter.p_no_starve.P_NO_STARVE_A

Change one bit in wrr_arbiter.sv and the md5 no longer matches - the certificate is now about a file that no longer exists.

Two ways to close the proof

Bounded (BMC). Check every state reachable within k cycles. Cheap, fast, and honest about its limit: a depth-12 bounded result says nothing about cycle 13.

Unbounded (k-induction). Prove a strengthening invariant holds forever, then show it implies the property. The wrr_arbiter no-starvation proof closes this way - the harness comment names the actual invariant set (INV_QUOTA_RANGE, INV_WAIT_QSUM, INV_QFIDX_LE, and three others) that bounds the per-round quota drawdown and makes the fairness argument inductive at depth 12. It is more work to find the right invariants, and it is the only one of the two that proves the property for every cycle, not just the first twelve.

VERDICT.txt states which kind you got, in plain text, for exactly this reason - a bounded result and an unbounded one look identical in a press release and are not identical claims.

Key Lesson: “Proven” is not one thing. Ask whether it is bounded to a depth or unbounded by induction - they are different guarantees, and only one of them is a proof for all time.

Proving it: the demo that tries to fail

The repo ships tamper_demo.sh, and its only job is to make the proof lie to itself and get caught. It flips one line in ring_buffer.sv - the write-ready condition, inverted so the buffer reports ready exactly when it is full - and re-runs the same sby task the certified verdict used.

step	what happens
patch	wready = !full becomes wready = full
hash	md5 of ring_buffer.sv no longer matches VERDICT.txt
re-run	sby -f fv_ring_buffer.sby prove
result	proof FAILS, failing assertion IDs printed, counterexample waveform written
revert	RTL restored, md5 confirmed to match the certified hash again

The script’s own comment states the stakes plainly: “if this script ever prints a passing proof, discard this repo and tell us.” That is the property we most wanted a stranger to be able to check without asking us anything - not that the proofs pass, but that they are capable of failing.

Key Lesson: The most persuasive thing a proof bundle can ship is not a passing result. It is a script that shows you the same proof failing on purpose.

From “it works” to “it ships”

• Reset is proven, not assumed. P_RESET_NO_GRANT and P_RESET_QUOTA check that quota clears to a hard zero on reset, not to the weight signal - a subtle bug class if the two get swapped.
• Parameterization is swept in one proof. The arbiter closes across three configurations at once (NUM_IN=2/3/4, including a non-power-of-two count), not one happy-path width.
• Toolchain is pinned, not assumed. ENVIRONMENT.txt names exact versions - Yosys 0.66+154, SBY 0.66-4-gd3e72d2, Z3 4.15.5 - and reproduce.sh runs under an “uncertified environment” banner if your local tools do not match.
• Non-vacuity is checked, not claimed. VERDICT.txt states plainly that “testbench assertions that re-state DUT definitions verbatim are constant-folded away before the solver” - the certificate counts the proof obligations that survive that folding, not the raw assertion count, which would overstate what was actually proven.
• Scope is stated, not implied. The README says it directly: formal is strongest on control logic and bounded data structures like these two primitives; a complex design also needs dynamic verification (UVM, coverage) alongside it, not instead of it.

Lessons

A proof bundle that cannot fail on tampered RTL is not evidence, it is a screenshot with extra steps. And a verdict with no RTL hash is a claim about some other file - hash-bind the certificate or you are trusting a description, not a proof.

The bundle

github.com/VoskenAI/vosken-certified-samples - clone it, run ./reproduce.sh, then run ./tamper_demo.sh and watch it fail on cue. The wrr_arbiter verdict there is our internal Tier A: unbounded proof (k-induction, depth 12), non-vacuous (every cover point reached under the same assumptions the proofs use), plus a mutation gate at sign-off (every hand-injected single-fault RTL mutant we tried against it was killed - source: the repo’s own VERDICT.txt). The same bundle layout - rtl/, formal/, a manifest, a signed release - is what ships behind every claim on our evidence page.

Where to go next

• The evaluator’s checklist, explained - the five questions to ask before you trust any bundle, this one included.
• A passing testbench proves nothing - until it can fail - the same falsifiability argument, aimed at UVM instead of formal.

Can I re-run your proofs in my CI?