Who checks the checker

A subject the papers are about. The loosest grouping, and the one to reach for last.

A proof about a chip is only as good as the thing that produced it. This set collects the works that turn the apparatus on itself -- verifying a prover, a checker, a solver's supporting algorithms, or the framework in which components are composed. Membership requires the verification machinery to be the object verified, not the instrument. **One member stretches that rule deliberately and the stretch is recorded rather than silent.** saravanan2025synfuzz does not *verify* anything: it fuzzes the gate-level netlist, finds seven new synthesis bugs and ten in Yosys, and demonstrates an attack that industrial logic equivalence checking does not catch. It is here because the object under test is the toolchain itself, and because excluding it would leave the set claiming that doubt about tools is only ever discharged by proof. It adds a fourth strategy to the three below -- **test the tool** -- and it is the only one of the four that has produced CVE numbers.

**A second deliberate stretch, added 2026-09-17, and it goes one level further out.** bhadra2026gatetruth turns the apparatus not on a prover or a synthesiser but on the **instrument used to judge them**: it applies mutation testing to the testbenches inside RTL design benchmarks, on the premise that "a testbench that never fails is not evidence of a correct design; it may simply never stimulate the logic that is actually broken." Pointed at RTLLM v2.0, 72 percent of 46 auditable designs fall below its 95 percent mutant-kill floor and three score zero; NVIDIA's CVDP cannot be audited at all because its public release withholds the reference solutions mutation testing needs. **A benchmark that cannot be audited from its public artefacts is a different object from one that fails an audit**, and the set should keep that distinction.

It earns its place for what it does next, which is rarer than any of its findings. It audits its **own** suite by the same standard, quantifies its exposure to Goodhart's law by re-measuring ten testbenches it had revised in response to mutation results, and then **retracts its own earlier account of that correction** -- the revision "partly consisted of the same unsound equivalent-mutant exclusion", so only three of the ten still clear the floor. The sentence to remember: "tuning toward the metric and quietly excluding inconvenient mutants from it were, in practice, the same revision effort." A separate finding in the same paper bounds every leaderboard this corpus might cite: a uniform 4096-token output cap silently truncated three of seven models, and re-running at 16,384 moved one from fifth place to first -- with the author holding only the two movements that clear a measured noise floor as established. **A benchmark that does not report its cap has not reported its experimental condition.**

So the set's strategies are now five: verify the prover, verify the checker, certify the result, test the tool -- and **audit the measuring instrument**.

**That fifth strategy now has two members, and the pair says more than either alone.** bhadra2026gatetruth finds benchmarks to be **weak instruments** -- 72 percent of one widely adopted RTL suite falls below the mutation-kill floor its author holds his own suite to. sarihi2024seekers finds them to **pose the wrong problem**: hardware-Trojan benchmarks publish where the Trojan is and how large, and "this enables the defense side to fine-tune their HT detectors to showcase strong HT detection rates", so a detector is scored on localisation-given-certainty when the real task is classification under uncertainty. Its reformulation, the Seeker's Dilemma, withholds even whether a circuit is infected, and it measures its own benchmark's difficulty by principal component analysis rather than asserting it.

**Stated together: a benchmark encodes a threat model, and a benchmark that encodes an unrealistic one produces numbers that are precise and irrelevant.** Both records are also honest in the way this set prizes -- one retracts its authors' earlier account of their own Goodhart exposure, the other publishes evidence that its instances are genuinely hard. A set about checking the checker should hold the cases where the *scoreboard* was checked, because a wrong scoreboard invalidates every result measured on it, including the ones this set otherwise reports approvingly.

**Seven members. Four of them doubt four different things, and three, all added later, show the question being decided in industry rather than argued in the abstract.**

- ridge2005mechanically verifies a **theorem prover**: a mechanically verified, sound and complete prover for first-order logic. - claessen2009faithful verifies a **semantics against an algorithm**: existing accounts of generalised symbolic trajectory evaluation were not faithful to what GSTE model checkers can actually prove, so the algorithms were incomplete with respect to them; this supplies a theory that deems a property true exactly when the tool can prove it. - davis2013verified verifies the **supporting code**: the And-Inverter Graph simplification algorithms that industrial equivalence checkers depend on are, in its own words, "implemented with optimized C or C++ routines with no guarantee of correctness", and it reconstructs them inside ACL2. - kastenbaum2021mechanically verifies a **composition principle**: assume-guarantee contracts are routinely used to prove abstractions sound, while the contract frameworks themselves had not been proved correct, so it formalises a generic one in Coq.

**The industrial three, and they turn the set's question into a decision with a price.** oleary2013relational states Intel's position outright: Forte's symbolic simulator is hard-coded into the internals of its functional language for efficiency, and while "the STE algorithm has been independently verified" there "are no plans to verify the highly engineered Forte internal simulator". slobodova2011flexible is the other side: at Centaur Technology the Verilog translator, BDD library and symbolic simulators "are written directly as ACL2 programs", so the engine is an object the prover can reason about -- and davis2013verified, already in this set for reconstructing AIG algorithms inside ACL2, is that same stack's work rather than an unrelated academic exercise. So the set's two poles are not a theorist and a practitioner but two shipping microprocessor companies, and the disagreement is about whether the cost of a verifiable implementation is worth paying. Note precisely what Intel does and does not claim: the *algorithm* is verified, the *implementation that runs* is not. khasidashvili2009assumeguarantee is the third, and it doubts something the other six do not -- not the prover, not the code, but the **hypotheses**. STE proofs hold under assumptions about the surrounding hardware; this translates those assumptions into System Verilog Assertions and checks them by simulation, finding tens of wrong or redundant ones and, in some cases, STE proofs that failed once the environment was corrected. A proof that passes because its antecedent is unsatisfiable is a fifth thing that can be wrong, and bryant1990ternary had named it in 1990.

**The distinction worth keeping is between doubting the theory and doubting the code.** Claessen and Roorda ask whether a semantics characterises the tool's reach -- an adequacy question. Davis and Swords ask whether the implementation computes what it claims -- a correctness question. A tool can be impeccable on one count and wrong on the other, and a corpus that holds only one kind of doubt will not see that. A third kind has since joined them: the assumptions under which the tool was invoked may not hold of the world the circuit is placed in, which is neither an adequacy nor a correctness question about the tool but a question about its use. And a fourth, visible only once the industrial records are in: whether anyone intends to check any of this at all, which turns out to be a budget decision made differently by companies of different size.

**Why this belongs in a bibliography about hardware.** The chain a hardware claim actually rests on is long: a design, a translation into a tool's language, a decision procedure, the graph algorithms underneath it, and a proof framework composing the results. This corpus documents the first two links heavily -- see the-cost-is-in-the-translation -- and the rest hardly at all. The set exists to make that visible rather than to suggest it is well covered.

**What was not here, and the correction.** This paragraph used to say the corpus held nothing on machine-checked proof certificates, that an arXiv sweep found a proof-theory literature with no hardware connection, and that the gap might be real because "the people verifying solvers and the people verifying chips publish in different places". That last inference was wrong, and bryant2021dual is the counterexample: the inventor of the ordered binary decision diagram, with Marijn Heule, making a BDD-based QBF solver emit a dual proof checkable in time proportional to the BDD operations performed. The two literatures are not separated by community; they were separated in this corpus because only part of one career had been collected. Bryant's publication index carries a further run of this work -- clausal proofs for pseudo-Boolean reasoning (TACAS 2022), translating pseudo-Boolean proofs into clausal ones (FMCAD 2024), certified knowledge compilation (SAT 2023, SAT 2025) -- none of it yet held. **The lesson for searching, not just for this set:** an empty result from one index is evidence about that index. Ask who, among the people already in the bibliography, went on to work on the missing thing.

nukala2024translating has since closed most of what that paragraph called missing. It is at **FMCAD**, the same venue as een2011efficient and khasidashvili2009assumeguarantee, it is about **DRAT** and its efficiently checkable variant LRAT, and it records that verified DRAT checkers exist in ACL2, Coq and CakeML and have checked proofs two petabytes in size. So machine-checked proof certification is ordinary practice in satisfiability, and the set can now say so with a citation.

**It also supplies the argument that organises this whole set**, from people who build solvers: "Creating a formally verified solver (using an interactive theorem prover, for example) would severely compromise the ability to optimize and rapidly evolve the program. An alternative to a formally verified solver is to have the solver generate a proof certificate for each execution." Three strategies, then, and the set holds all three: **verify the tool** (davis2013verified, ridge2005mechanically), **trust the tool** (oleary2013relational), **certify each answer** (bryant2021dual, nukala2024translating).

A *verified SAT solver* is now held too: andrici2019verifying, DPLL in Dafny — and since 2026-10-10 its extended version andrici2020who, whose figures supersede it and should be the ones quoted. Take it with its own caveat -- DPLL, not CDCL, fixed variable ordering, and "not currently competitive against state-of-the-art CDCL solvers" -- but it supplies two things the set had been asserting without evidence. First the premise: fuzz testing has shown that many state-of-the-art SAT solvers contain bugs, **including soundness bugs**, and such a bug "may lead the verification tool to prove correct a wrong program". Second the price, now measured three ways in the later version: 3088 lines of Dafny at a **four-to-one ratio of proof to code**, an extracted solver with negligible overhead against the same algorithm written directly in C#, **roughly a factor of two slower than the same algorithm in C++**, and far behind MiniSat — which the authors attribute to CDCL being exponentially faster than DPLL rather than to verification. So the corpus can now separate what verification costs from what the algorithm costs, and the first number is about 2x -- which is precisely the cost nukala2024translating cites when it declines to verify solvers at all. It also dates the field's institutional answer: since **2016** the SAT competition has required main-track solvers to emit independently checked UNSAT certificates. And it marks where certification runs out: a satisfiable instance yields a witness anyone can check, but for unsatisfiable ones the certificate "could be exponentially large or the SAT solver might not be able to output certificates", and then the implementation must simply be trusted. The three strategies are therefore not interchangeable.

**That gap is now partly closed.** seufert2026certified is a *certifying sequential equivalence checker* -- certificates emitted for real retimed and resynthesised circuit designs, with a certificate transformation that carries the guarantee back across the retiming preprocessing, so the uncertified step used to make the problem tractable is not left outside the claim. Its own framing is the sharpest statement of this set's question applied to industry: it is "problematic to make use of (uncertified) retiming steps to prove the correctness of (sequential logic synthesis and) retiming". It also prices certification -- comfortably ahead of the certifying competition winner, merely "competitive" with ABC, which certifies nothing.

Still absent: the last link, from such a certificate to a claim about a **fabricated** circuit rather than a netlist. Every record here stops at the design. Note that even the certificate papers do not claim the whole chain -- nukala2024translating names its own unverified CNF encoder as "a weak link in terms of the trustworthiness of our toolchain".