The cost is in the translation

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

Before anything can be proved about a chip, the chip has to be restated in a language the proving tool can hold. This set collects the works where that restatement is the work -- a semantics, a mapping, or a translator built so that a verification technique can reach a design written the way designs are actually written. Membership requires the translation to be the contribution or an acknowledged prerequisite, not an implementation detail.

**The set exists because the same step keeps being taken, by different people, for different tools, across three decades.**

1992 boulton1992hol a HOL semantics for a subset of ELLA 1995 gordon1995semantic the complaint: Verilog has almost no theory, and a formal semantics is challenge one 2003 dumitrescu2003construction a VHDL to finite state machines translator, built to make the experiments possible 2006 toma2006verification VHDL into recurrent equations on time, deliberately prover-neutral, demonstrated with ACL2 2009 garavel2009semantics CHP given a structural operational semantics, then translated into LOTOS for CADP 2018 bouzafour2018modelchecking a synthesisable SystemVerilog subset mapped into LNT for CADP 2024 oulkaid2024transistor a transistor netlist given a relational semantics and discharged with Z3

Those seven were the set as first written, and between them they name six target formalisms with no two agreeing on where the design should be sent: HOL, finite state machines, recurrent equations, LOTOS, LNT, SMT. The list above is kept as the set's origin rather than its contents -- later members are named in the positions below.

**What the set argues.** toma2006verification names the obstacle exactly: theorem proving is hard for designers because "the model of the design is described directly in the logic of the tool". Every member is an attempt to remove that requirement, and the recurrence is the evidence -- if translation were a solved or minor step, it would not be the headline contribution of a doctoral thesis in 2003 and again the headline contribution of a conference paper in 2018.

**Two members show the cost is not merely effort.**

bouzafour2018modelchecking applied its SystemVerilog-to-LNT mapping **by hand** to a 4000-line industrial memory protection unit, and lists building the translator as future work "while eliminating the potential errors that may arise from manual translation". So what the model checker proved holds of a model a person wrote from the design, not of the design. garavel2009semantics by contrast reports an implemented translator, which is why the two are linked.

oulkaid2024transistor shows the same problem one level down, where the source is not a language at all but a netlist, and the translation has to decide how much of the transistor's electrical behaviour to admit. Its companion thesis measures three such choices against each other and finds the most accurate one unsound -- so at that level the translation is not just a cost but a place where soundness can be lost.

**The honest counter-argument**, worth stating because the set could otherwise read as a complaint: translation is also what makes verification usable by anyone other than its authors. boulton1992hol says so directly -- formal techniques "are not well integrated into the set of tools more traditionally used by designers" -- and giving ELLA a semantics inside HOL was the proposed integration. The members are not lamenting the step; they are doing it, repeatedly, because nobody has made it unnecessary.

Overlaps what-one-proves-with, which collects the tools themselves. The distinction: that set is about the prover, this one is about the distance between the prover and the artefact. **Since that was written the set has kept growing -- fourteen members as of 2026-09-23 -- and the additions do not all translate in the same direction. Seven positions are now represented, and naming them is the most useful thing this description can do.** (Any count in this description is a dated observation, not a total; it has been stale twice.)

**One: translate the design into the tool's language.** The original shape of the set. boulton1992hol gives ELLA a semantics inside HOL; dumitrescu2003construction builds a VHDL-to-finite-state-machine translator before its experiments can run; toma2006verification maps VHDL into recurrent equations on time, deliberately prover-neutral; garavel2009semantics translates CHP into LOTOS; bouzafour2018modelchecking maps a SystemVerilog subset into LNT, **by hand**, with automation left as future work.

**Two: translate the specification instead.** ploix2025comprehensive leaves the RTL alone and translates the architecture's own Sail description into SystemVerilog, so the reference model is the definitive one rather than a re-statement. The direction is reversed and the gain is that nobody has to be trusted to have restated the specification faithfully.

**Three: verify the translator.** law2026mechanized formalises dataflow circuits in Rocq as a first step toward a high-level synthesis compiler proved to preserve semantics. This is the position gordon1995semantic asked for in 1995 when it listed correctness of synthesisers among nine open challenges, and the corpus waited thirty-one years to hold an attempt at it.

**Four: do not translate at all.** jules2025herve writes the processor in Kôika, a hardware description language embedded in the Rocq proof assistant, so design and proof share a language. It is in this set precisely because it looks like an escape from the set's problem and is not: the cost reappears as the restriction to what such an HDL can express and compile into. oulkaid2024transistor is a limiting case in the other direction -- the source is a netlist rather than a language, and the translation must decide how much electrical behaviour to admit, which is where its companion thesis finds soundness can be lost.

**Five: translate automatically, then audit the output.** sarma2026controllerdatapath leaves high-level synthesis unverified and checks each generated netlist instead, on the ground that HLS "was never developed with security in mind" and its optimisations can destroy side-channel resistance **while keeping functional correctness intact**. puri2014using is the same problem answered from position three -- certifying the loop pipelining transformation in ACL2 -- and states the trade explicitly: interactive proof is acceptable once per transformation but not once per design, because a dedicated team of proof experts may not exist. The two are the standing alternatives, and the corpus holds one of each for the same class of tool.

**Seven: translate sideways, into software.** trippel2021fuzzing converts register-transfer-level hardware into a C++ model with Verilator and turns a coverage-guided software fuzzer loose on it. Every other position in this list sends the design toward a *verification* formalism; this one sends it toward a *programming language*, to inherit a toolchain rather than a logic. The paper is explicit that the cost is the mismatch between execution models, and enumerates it: how to represent a test case, what the hardware equivalent of a crash is, what counts as coverage, and how to write a design-agnostic harness. Its answer to the second -- invariant violations and golden-model mismatches -- is where the translation's price is paid, since the method then finds only what the assertions or the reference model already describe.

**Six: translate back.** yin2025boole is the position nobody plans for. Synthesis and technology mapping leave the netlist functionally correct and structurally unrecognisable -- "carry-chains and adder trees are often fragmented or altered... rendering them unrecognizable" -- so the word-level structure a verifier needs has to be **reconstructed** from gates by equality saturation over e-graphs. It supplies this set's thesis as a pair of numbers: 11 seconds to recover the structure of a 24-bit multiplier, after which verification falls from 32,402.74 seconds to 0.07. The restatement is not merely the cost of verification; on this evidence it is almost the whole of it.

**A note on baty2024formal**, which sits in two positions at once and should not be filed under either alone: it builds its processor inside the prover in Kôika (position four) *and* ports FIRRTL, an industrially used HDL, into Coq (position one). The thesis does both rather than arguing for one, which is the clearest sign that neither position has won.

**Six members added between September and October 2026 were not named above; they are placed here rather than left to be rediscovered.**

*Position four, the design lives in the prover, gains its whole family.* choi2017kami is the root -- Kami, a Coq embedding of Bluespec-style rule-based hardware, extracted to FPGA. bourgeat2025making is its authors' own diagnosis of it: giving modules a semantics over arbitrary sets of simultaneous method calls makes proof cases grow **exponentially in the size of a module's interface**, and the fix is a language restriction. kurze2026nocout keeps the semantics and adds a program logic instead. Together they show the position is not one choice but an argument still in progress, and that its cost is paid in proof-case explosion rather than in translation effort.

*Position three, verify the translator, gains a finished instance.* wang2026formally proves one pass of the FIRRTL compiler -- width inference -- correct in Rocq, on a pass whose official implementation throws an exception on the simplest circular case. Unlike puri2014using, which reports its proof as ongoing, this one completes and extracts a runnable implementation.

*Two new positions, both about avoiding the gap rather than crossing it.* zhao2026formally describes each operator **once** and renders synthesisable SystemVerilog, an SMT model and a Lean model from that single source, so "they are the same dataflow graph printed in three syntaxes" -- the translation cannot introduce a divergence because there is only one description. (Read its provenance caveat before relying on it.) And lyu2026rtl2lean goes the opposite way from every other member: it takes **SystemVerilog that already exists** and lifts it automatically into Lean with a layered theorem library, which is the case industry actually has. The first prevents the gap by construction; the second closes it after the fact.

**High-level synthesis joined the set on 2026-09-17, with two members taken the same day and meant to be read together.** Both concern a compiler that turns C into RTL, and between them they say that what HLS preserves and what a hardware designer needs preserved are not the same list. sarma2024maskedhls is the loss case: the front-end optimisations are all value-preserving and one of them, expression balancing by associativity and commutativity, reassociates a masked cryptographic gadget so that shares which must never meet now meet in one term. The translation is correct in the value domain and destructive in the power domain, and nothing in the toolchain knows the second domain exists. lee2026separation is the opposite attempt: it tries to establish a structural property the compiler cannot express, modelling physical SRAM banks as separation-logic spatial predicates over the LLVM IR so that two concurrent accesses to one bank become the contradiction P * P implies false, discharged by an SMT oracle. It is here on its soundness theorem, which licenses a claim about RTL execution traces from algebra over SSA variables -- the same licensing move as the adjunction in winskel1987relating. It should be flagged as an unrefereed single-author preprint with no implementation and no measurements: its own future-work section says the LLVM pass and the benchmarking are still to come.

**A recurring failure shape, visible once three records taken in one week are read together.** In each, correctness is established upstream and lost at a downstream step that was licensed at a level where the property is not visible. sarma2024maskedhls: the source program is masked, and high-level synthesis reassociates the expression. bouesse2005dpa: the logic style is dual-rail and transition-balanced by construction, and place and route unbalances the load capacitances of the two rails. bozga2002verification: the circuits are speed-independent by construction and therefore, on the face of it, need no verification at all -- but the synthesis tool SIS maps them onto standard cells with fan-in two, and that mapping "does not take into account potential hazards that could be generated by internal signals". Timed-automata analysis then finds real bugs in two of them.

Three different properties -- side-channel resistance, transition balance, hazard freedom -- three different downstream tools, and the same structure: **a guarantee that is true of the design is not true of what the flow emits, because the transformation is correct by a criterion that does not mention the guarantee.** That is this set's thesis stated as a fact about practice rather than as an argument, and it is why the set collects translators rather than only proofs. Note also what it implies about "correct by construction": the phrase names a property of a design discipline, and every step after the discipline is a place to lose it.

**And it was named as the next problem in 2004, which the set should record so the pattern is not mistaken for a recent discovery.** boubekeur2004validation builds two validation environments for CHP specifications inside TIMA's TAST flow, reports a first attempt at verifying *after* synthesis, and judges it a failure: verification at that level "reste une tache difficile". The remedy it proposes is exactly the missing piece -- analyse the transformations performed during synthesis, find correspondences between the circuit before and after, and build a **refinement relation** so the synthesised circuit can be verified against its specification. Twenty-two years later the records above are still paying for its absence. A bibliography is useful here in a way a literature search is not: it can show that a gap was correctly identified, correctly diagnosed, and not closed.

**The strongest form of the pattern arrived on 2026-09-17, and it should be stated at full strength because it removes the easy explanation.** pesin2025formally adds two control-flow fault-injection countermeasures to **CompCert**, proving both that they do not change observable behaviour without faults and that, under a fault model added to RTL's semantics, every attack in the model is caught or has no observable effect. Then the same compiler's **verified optimisation passes remove part of the protection**: measured with symbolic fault injection, "when optimizations are also activated, some one-fault traces subsist for all examples except aes."

**A verified compiler did this, and not by being wrong.** CompCert's theorem preserves *observable behaviour*; robustness is not observable behaviour, so nothing obliges the back end to keep it. The guarantee is lost because the tool is right about something else. The authors name what is missing -- a robustness-preservation theorem, requiring changes to the backend's deterministic semantics and forward-simulation framework -- and do not claim to have it. Which is boubekeur2004validation's 2004 diagnosis, a refinement relation across the transforming step, restated for a machine-checked compiler twenty-one years later. **No member of this set has yet closed that gap; several now state it precisely.**

**And the diagnosis sharpened again on 2026-09-17.** michelland2025compilation argues that the threats "are inherent to the descent in abstraction and can't simply be dodged by disabling optimizations", because compilation proceeds through several intermediate languages and the **lowerings between them are threats in their own right**. So this set's observation is not, after all, about optimisers: it is about abstraction descent as such, and turning the optimiser off buys less than the 87.99-percent-versus-42.68-percent runtime price pesin2025formally measures for doing so. His framing of why is the best this set holds: **"the interfaces between layers only isolate functionality. For every other aspect, such as performance or security, one has to consider the system in all its glorious complexity."** Assembler abstracts hardware functionally and has no mechanism for abstracting *faults*; and inside software, a compiler "will proudly delete the duplicates, which are redundant in its functional-only abstract semantics".

**Three answers to one gap, and they are worth distinguishing.** boubekeur2004validation proposes a refinement relation across the synthesis step; pesin2025formally names a robustness-preservation theorem for a verified compiler; michelland2025compilation builds **Tracing LLVM**, which carries an explicit connection between the source and intermediate programs so a countermeasure can navigate the abstraction stack. Two theorems nobody has proved and one channel somebody has built. The engineering answer comes with the honest report that it does not yet hold end to end: failures occur "because protections aren't end-to-end (e.g. wrappers don't survive past the instruction selector)" -- **the very failure the tool exists to prevent, occurring inside the tool.**

The record also prices the tension, on a RISC-V SiFive U740: median runtime loss 87.99 percent with countermeasures and no optimisation, 42.68 percent with optimisation on. Optimisation halves the cost of the protection **and** demonstrably weakens it, so the choice a designer faces is not academic.

**Two Intel/Arm members added 2026-09-17, and between them they say why one translation is never enough.** oleary2014modeling generates THREE representations of one algorithm from a single hand-coded SystemC source, because "some of the requirements of high-level synthesis are in conflict with those of readability and formal analysis": a synthesisable C++ variant for the tool, a MASC model for documentation and mathematical analysis, and an ACL2 translation for proof. **A single source that is synthesisable, readable and provable does not exist**, and the arithmetic boundary is where the split falls -- MASC arithmetic is unbounded like ACL2's, SystemC's is not. russinoff2020formal is the later industrial form, and it prices the abstraction: the hand-coded RAC intermediate model makes Arm floating-point units "approximately 85 percent" smaller in code than the Verilog, where the AMD and Centaur routes produced ACL2 "at least comparable in size to the Verilog source". **And it moves the trust rather than removing it:** the hand-written model need not be trusted because a commercial equivalence checker relates it to the RTL -- so what must be trusted is the checker, the translator and the arithmetic library.

**A 2013 member where the translation exposed a missing definition rather than a missing proof.** vangastel2013formalisation formalises the semantics of Intel's xMAS fabric language in ACL2 -- eight primitives, typed channels carrying irdy/trdy/data -- and gets five of them, termination, non-empty routing and correct flow control. The three it leaves are fork, merge and join, the ones that arbitrate and synchronise; and the reason is not proof difficulty. Extending to message-dependent routing "requires a re-definition of the notion of correctness... When routing depends on the content of a message, and functions may change this content on the way, it is no more obvious which destination is the correct one." **A correctness notion that dissolves when the mechanism gets richer** -- the same thing fabian2026detecting says about speculation and the masking records say about levels. The semantics also holds only where there are no combinatorial cycles, which is this set's usual side condition in another dress.

**THE FINDING THIS SET CAN NOW STATE AT FULL STRENGTH, as of 2026-09-18: every layer that transforms a design or a model has been found wrong by somebody who checked it, and the checking was always a side effect of building something else.** yin2025hec verifies MLIR source-to-source transformations by equality saturation and "identified two critical compilation errors in mlir-opt: loop boundary check errors causing unintended executions during unrolling, and memory read-after-write violations in loop fusion that alter program semantics" -- **a production compiler optimiser turning programs into different programs.** Beside it: mukherjee2016equivalence found an ARM FPU's RTL disagreeing with its own C model after synthesis; hunt2022vwsim found bugs in JoSIM while rebuilding it in a logic; canakci2022processorfuzz found a bug in a golden reference model; waddoups2025probabilistic found an error in a published probabilistic model while reproducing it. **And the industrial synthesis compilers themselves, with vendor confirmations, added 2026-09-18:** xu2025structural differentially tested FPGA logic synthesis across Yosys, Vivado, Iverilog and Quartus for three months and reported sixteen unique bugs, **twelve confirmed by official technical support and six already fixed** -- among them a buffer overflow from inadequate input validation, a memory leak from unreleased allocations, an incorrect state machine transition due to a race condition, data corruption from improper concurrency handling, and several bare synthesis crashes named after the internal function that died. The tools that compile safety-critical hardware crash on valid input and leak memory, and unlike the other entries in this list that finding was the point of the work rather than a side effect of it. **And then there is the case where the wrongness is the weapon, added 2026-09-18.** solt2025lost fuzzes for TRANSLATION bugs -- mistranslations that raise no error and no crash -- and builds them into gadgets: a construct that "produces 1 under normal circumstances, and 0 under a translation bug", so that malicious behaviour "does not register during validation, but appears in the synthesized hardware", or is "injected by the synthesizer" while every simulator reads the design correctly. Twenty translation vulnerabilities among 31 bugs and 25 CVEs in Verilator, CXXRTL, Icarus Verilog and Yosys, then a CVA6 RISC-V core leaking supervisor memory to unprivileged software, undetectable in all three simulators. **The design is benign under any reading of the language and the malice is contributed by the tool** -- so a proof about the source is not a proof about the artefact, and that gap is now an exploitation technique with CVE numbers rather than a caveat in a note. **A member where the translation restricted what could be designed, added 2026-09-18.** feng2026generalizable adapts Verilog and Standard Delay Format -- notations built for level-based logic -- to superconducting **pulse-based** SFQ gates, where information is a flux quantum passing rather than a level held. Earlier attempts needed support modules because "specify timing blocks do not support references to SystemVerilog interfaces", and the workaround hardened into a limit: the destructive pulse consumption "was inherently tied to the modules, preventing the ability to model non-destructive read out cells (NDRO) or extend this framework to asynchronous gates". **The abstraction could not express a cell type, so that cell type stayed outside the flow.** One physical fact from it inverts a CMOS habit: "in SFQ circuits, interconnect delays typically represent a majority of the clock period", so the wire is the thing and the gate is the correction.

**Six now, and the sixth is the cheapest.** serwe2015formal rewrote a LOTOS model of the DES into LNT and the rewrite alone "uncovered a few errors in the LOTOS definitions of the S-boxes and a small bug in the LNT2LOTOS translator", and additionally "showed that the controller was too restrictive" -- over-serialised relative to what the design permits. **Writing the same model twice found a fault in the model, a fault in the translator, and a fault in the design's control.** Its other check is method worth copying: a prototype generated from the specification was run against publicly available DES implementations, which caught "typographic errors, i.e., bad copying of the DES standard" into both models. **Seven, and the seventh is the highest layer of all: the prose standard.** tan2025formalising built an Isabelle model of CXL.cache from "the English prose specification" and thereby found parts "unclear, ambiguous or inaccurate", some of which "could lead to incoherence if left unfixed" -- **and the CXL consortium accepted nearly all the proposed fixes.** Their example is a sentence with two readings, both wrong: "the host is only allowed to have one snoop pending at a time per cacheline address per device" is ambiguous "because per appears more than once", and neither reading is correct, since multiple pending snoops on one cacheline are legal within a single transaction. **A defect at this layer does not produce one wrong chip; it produces incompatible chips**, which is why the authors open by noting that multiple vendors will implement the standard. **And an eighth of a different kind: what failed was not an artefact but a theorem's scope.** trippel2017tricheck checks the language, compiler, ISA and microarchitecture TOGETHER rather than in isolation, and found "two counterexamples to the **supposedly proven-correct** trailing-sync compiler mappings from C11 to the Power and ARMv7 architectures" -- plus a RISC-V-compliant microarchitecture that "incorrectly allows **144 outcomes forbidden by C11**" across 1,701 litmus tests. **A legal implementation of the ISA breaking the language's memory model, and a published proof refuted from outside the layer it covered.** **The interesting failures are between layers, each of which may be correct on its own terms** -- which is this set's thesis stated as a result rather than a worry. Its opening case is the timing lesson: the ARM load-to-load hazard left buggy microarchitectures in the field, so ARM changed the architecture to match the hardware that already existed, where tan2025formalising got ambiguities fixed in CXL *before* vendors implemented them.

**Seven layers, seven independent discoveries, none of them the point of the paper that made it.** HEC is also the member that closes its own rule-justification gap -- algebra for static rules, Z3 for dynamic ones -- where coward2024rover leaves it open.

**A 2026 member where the translation is meaning-preserving and still changes everything, added 2026-09-18.** aditi2026robustness rewrites RTL in ways that cannot alter behaviour -- reversing commutative operands, renaming identifiers, adding parentheses -- and regenerates assertions: **"in every model-transformation condition, some behaviors that are correct on the original RTL become incorrect after transformation", with invariance failure between 9.7 and 27.0 percent.** Reparenthesisation was the worst. **And the metric lesson is sharper than the rate:** there are "cases where aggregate accuracy improves while previously correct behaviors regress" -- **a single number can rise while the tool breaks what it used to get right.** This set already holds rewriting as the central operation of modern tooling (coward2024rover, cheng2023seer, yin2025hec, and tanaka2026relational's fivefold swing from an index direction); this is the record showing the *verification artefact* moving when the source is reshaped.

**What they have in common.** In none of them is the translation a detail of engineering. It is the step that determines what can be proved, who has to be trusted, and where the argument can fail -- which is why a corpus about hardware correctness has to hold the translators and not just the proofs.