Proved here, used there

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

A correctness claim is never about an artefact. It is about a description of one — a netlist, a state machine, a lattice of signs, a term in some logic — and the artefact is elsewhere, obeying physics. So every verification eventually owes an account of why what was proved of the description holds of the thing, or at least of the next description down. This set collects the works where that transfer is the subject rather than an assumption.

Membership is narrow on purpose. Working at some level of abstraction is not enough, or the set would swallow most of the corpus; the work must take two descriptions and say something about what carries between them. Fifteen members, answering in four distinct ways. The most recent arrives from an unexpected direction: seger1995formal, the founding paper of symbolic trajectory evaluation, works on a state space **ordered by information content** whose elements stand for sets of concrete states, and proves that every trajectory formula has a unique weakest satisfying trajectory. A lattice of approximations, a best approximation to a given description, soundness carried by the order — the machinery is recognisably cousot1977abstract's Galois connection and winskel1987relating's adjunction, reached independently by people building a hardware verifier. Its authors do not call it abstract interpretation. Winskel's parenthesis in 1987 said the literature on abstract interpretation might be useful here; this is what that would have looked like. mateescu2020modeling is the one that shows the levels are not equally capable: a patented attack-detection shield modelled at circuit level and at gate level, where the coarser model supports an induction proof that the shield is secure at arbitrary size and the finer one does not, because gates in isolation need stubs. Refine the model and you can lose the ability to generalise the result.

Three of them do the thing the set is named for by **giving a design language a meaning in a logic**, so that what is verified is the image of a design rather than the design, and the embedding is what licenses carrying the result back. boulton1990hol embeds a subset of ELLA, the Royal Signals and Radar Establishment's commercial language; vantassel1993femtovhdl gives a structural operational semantics for a subset of VHDL, which as an IEEE standard had none; Van Tassel is an author of both. Each is explicit that the fragment given a meaning is deliberately small, and boulton1990hol says there are semantic issues that may affect the ease of verification — the honest form of the admission this set exists to collect.

Two do it by **proving one artefact's two descriptions equivalent**. wong1993formal takes VIPER's ALU as a function over two 32-bit operands and as a structure of 4-bit slices and proves functional equivalence in HOL; thirty-three years later zhu2026equivfusion does the same job across abstraction levels by handing both descriptions to a solver. Deduction against decision procedure, same question.

**Prove the relation once, and mathematically.** winskel1987relating takes two models of hardware — his own compositional MOS model and Gordon's simpler two-valued relational one — and derives by an **adjunction** the conditions under which an assertion proved in the cheap model holds in the accurate one. cousot1977abstract does the same thing for programs ten years earlier and from an entirely different community, describing computations "in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations", with soundness carried by a Galois connection. A Galois connection is an adjunction between posets. Two fields, a decade apart, reached for the same device to answer the same question, and the corpus holds both without either citing the other. That coincidence is the best argument this set exists.

**Make the obligation payable once rather than every time.** melham1988abstraction states the question for hardware in 1988, as a chapter of the Kluwer volume that also carries Winskel's model; melham1990formalizing is the thesis-length answer two years on, and it supplies the move that makes the whole programme affordable: the conditions licensing an abstraction are dischargeable **once per circuit design style**, not once per circuit. That is an economic claim as much as a logical one, and it is what separates a technique from a curiosity. The 1988 chapter is held as a citation only, paywalled at Springer.

**Or refuse the split, and speak one language at every level.** moszkowski1985temporal takes the interval rather than the instant as primitive, so a fast thing and a slow thing can be described in the same logic and the relation between them stated rather than assumed. The title's promise is multi-level reasoning, and the formalism travelled: two of this corpus's Cambridge-adjacent hardware records use it for timing. Held as a citation; IEEE Computer 1985 is outside the gate.

**Or relate nothing at all, and check each pair by brute force.** zhu2026equivfusion lowers PyTorch, C, Chisel, Verilog and gate-level netlists into one intermediate representation and asks an SMT solver whether any two specific artefacts agree. Nothing is proved about the relation between the levels; nothing transfers to the next design. Against that, it accepts arbitrary source languages and needs no theory of what a design style is.

**The trade the set exists to display is reuse against reach.** Winskel, Cousot and Melham buy reuse: prove the relation, or the design-style conditions, and every later instance is cheap — at the cost of a heavy formulation up front and a commitment to one pair of models. EquivFusion buys reach: no formulation at all, any pair of languages, and every instance costs a fresh solver run. Note which way the chronology runs. The mathematically ambitious answers are the old ones; the 2026 tool is the least ambitious and the most widely applicable, and its own evaluation is three toy circuits. Whether that is the field maturing or forgetting is exactly the question a reader should bring to these six.

Overlaps the-switch-or-the-curve, and the distinction is worth stating because three records sit in both — winskel1987relating and the two Melhams. That set asks how much of the *device* a correctness argument admits — switch, or curve. This one asks whether a claim, once proved, *travels*. A work can commit to a rich device model and say nothing about transfer, or transfer beautifully between two models that are both wrong about the silicon.

Known gaps, so the next reader does not mistake absence for judgement. Halpern, Manna and Moszkowski's A Hardware Semantics Based on Temporal Intervals -- the semantics behind the fourth member's exposition -- is now held as halpernhardware, a citation without a copy: ICALP 1983, pages 278--291. The year took work worth recording. Crossref and OpenAlex both point at 2006, which is when Springer back-deposited the DOI, and the whole volume is dateless — all forty-three of its chapters carry a null issue date. Semantic Scholar settled it twice over, giving 1983 outright and a DBLP key of conf/icalp/HalpernMM83 whose trailing stamp says the same thing independently. **The set's cleanest crossing of the gap, added 2026-09-18, and it runs the wrong way.** trippel2018meltdownprime synthesises attack programs from a microarchitecture model and a threat pattern using Alloy; given Prime+Probe it produced two variants nobody had proposed, and **SpectrePrime was compiled and run on an Intel x86 processor, averaging 99.95 percent accuracy against 97.9 percent for hand-written Spectre on the same machine**. Everywhere else this set must record that a result holds of a model; here the model's output was executed on the part. **A leak found in a description turned out to be a leak in the silicon** -- and the channel is the coherence protocol's own invalidations, which ravi2024qed assumes correct and tan2025formalising formalises.

**And a member where the transfer is checked by brute force.** coglio2018adding reports on the ACL2 x86isa model, a specification detailed enough to execute at "around 300,000 instructions/second in the system-level view and 3 million instructions/second in the application-level view" -- and that speed is an epistemic instrument, not a boast: "as a direct consequence, it has been possible to extensively validate the 64-bit model by running co-simulations against Intel's x86 machines, thereby increasing confidence in the model's accuracy." **A formal specification fast enough to be tested against the part it describes is the strongest answer this set can get short of a proof about silicon.** Two caveats belong with it, both the authors': the 32-bit extension this paper adds "ha[s] not been validated against actual x86 processors", and co-simulation is agreement with the processors that were available, not a theorem about them. Its incidental finding is worth keeping too -- **the legacy mode is the expensive one to specify**, because 32-bit mode uses segmentation "in its full glory" where 64-bit mode had let the model assume effective addresses were linear addresses, and withdrawing that assumption changed memory-access signatures and broke proofs built on the old shape.

**A 2016 member where the transfer failed and was caught, added 2026-09-17.** mukherjee2016equivalence takes the industrial route from a C model to Verilog RTL and checks each step: the C software model of an ARM floating-point unit proved equivalent to an IEEE 754 reference, while the RTL **did not** match that software model -- a bug in FP-MIN and FP-MAX when both inputs are NaN, attributed to "bugs in the high-level synthesis tool or during manual translation". **The description was right and the next description down was wrong, in a commercial part.** The paper also records why the standard instrument cannot be used across that gap: sequential equivalence checkers rely on "functional equivalence points" between the two descriptions, and an untimed C model and a pipelined RTL have none, so the transfer must be checked by bounded analysis instead of by correspondence. **This set's question is usually asked about physics; here it is asked about a compiler, and the compiler failed.** Compare tanaka2026relational, where the same tool layer got the cost wrong by a factor of five rather than the function wrong.

It holds no data-refinement classic, and no Milner-style treatment of when one process may stand for another, though camilleri1986hardware points at CCS and CIRCAL as the roads not taken at Cambridge. Those are the obvious next members.