Auditing published circuit databases against certified ground truth

Logic synthesis and circuit tools ship tables of small circuits that are called optimal: rewriting databases indexed by NPN class, lookup tables for three-input subcircuits, tables of minimum formula sizes, and per-function gate counts for cryptographic S-boxes. A tool that consults such a table inherits the label, and the label is rarely accompanied by anything a third party can check. We describe an audit protocol that tests a published table against ground truth produced by exact synthesis: a fixed snapshot, an exact encoding of the table's cost model, a descending SAT search in which a timeout is recorded as undecided, DRAT proofs checked by drat-trim for the decisive refutations, an independent re-simulation of every circuit, a reading of the consuming tool that separates the entries it can reach from those it cannot, a partition into classes on which cost is invariant so that one decided entry settles its class, and cross-checks between databases used only to refute. We report what the protocol found on seven published sources. On the 614,187-entry AIG database of the Simplifier tool it decided all 7,433 classes the tool can reach, lowered two of them, verified 204 proofs of up to 4.0 GB, and showed that 10,390 of the 10,449 improvements lie in entries the tool never looks up. A second database by several of the same authors stores the same two classes at the same non-minimal sizes. In a widely used synthesis library, a database labelled size-optimum since 2018 is above the minimum in 13 of the 135 classes it covers, and the complete database in the same file already shows it without a solver; we reported it as lsils/mockturtle#714 on 15 October 2026. A table of minimum formula sizes prints a total that its own columns contradict; we reported it to the authors on 15 October 2026. In a recent preprint on gate elimination, one lemma does not state a tree condition that its induction needs, the base case of one algorithm fails under one reading of its input condition, and one step of another algorithm undoes its own restriction as we read it; each is shown on an instance small enough to check by hand. An audit of a paper on simple circuit extensions found no error of content. In a paper on S-box implementations, the depth-1 AND counts of 26 of the 27 five- and six-bit S-boxes match what our exact depth-1 routine returns as the minimum, with the certification status of each lower bound in Section 6, one count can be lowered from 9 to 8, and one linearity value disagrees with the S-box it describes. As far as we can tell, neither reproducing the published pipeline nor counting how many sources agree would have exposed the findings on the Simplifier and Cirbo databases or on the preprint: reproduction re-derives the upper half of an optimality claim, and agreement multiplies upper halves. The table of formula sizes, the linearity value and the supplementary circuit for Q2260 mark the boundary of this claim, because recomputing or simulating from the source exposes all three, and the library label is not an instance of it. We relate the protocol to the refutation gap recently named by Pandey and state which of our own verdicts are still bare solver output.