Self-Consistency, Not Independent Verification: An Independent Audit of What "PROVEN" Means in EquivSVA

A PROVEN verdict from a formal engine is commonly read as “this assertion independently verifiesdesign intent.” We audit the public AI-assertion dataset EquivSVA and report three findings: (1)in 80 of 120 behavioral families, gold properties and RTL are generated from the same spec.json,and the generator reproduces them byte-for-byte; the remaining 40 are not covered by this conclu-sion. (2) 131 invariants receive no reachability witness, while the generator’s own comment stillclaims “Reachability/non-vacuity witnesses.” (3) Of 93 formally sound properties, 79 (85%) are notdistinguished by any of 3 controlled mutants, with UNKNOWN = 0 ruling out non-convergence.We therefore read PROVEN as “self-consistency of two co-generated artifacts,” not “independentcharacterization of intent.” We do not claim EquivSVA is defective, nor that its formal resultsare wrong; we bound the reading “PROVEN = independent verification” along source, coverage, andfailure-mode axes. A minimal reproducibility package reproduces at least three core findings onpublic data.