The switch or the curve

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

A transistor is a switch that is either on or off; a transistor is also a device with a current-voltage characteristic. Proof needs the first and silicon obeys the second, and this set collects the works that choose between them and the works that pay for the choice. Membership turns on the modelling level being the subject, not on the method or the era: a record belongs here if it commits to how much device a correctness argument admits.

Fourteen members, and the set now has three parts.

**What no model can promise.** marino1981general proves that no physical implementation of a non-trivial digital circuit can deterministically avoid, resolve or detect metastability. That is a floor, not an engineering difficulty: no mapping of every signal onto {0,1} can be sound about a circuit at all times, however carefully built. friedrichs2018metastabilitycontaining shows what it costs in the plainest possible terms — with a metastable input, a circuit computing ¬x ∨ x "may output an arbitrary signal value: 0, 1, or again a metastable signal", which is not the case for an unknown but Boolean x. The boolean model does not merely fail to see things; it is wrong about its own tautologies.

**The choice, and its blindness.** Cohn is read first and read for her caveats. cohn1987proof verifies the VIPER microprocessor in HOL and warns against "a false sense of security afforded by an HOL proof" since "there are many classes of errors not even visible in the models used"; cohn1988correctness turns that into the general statement the set is organised around — "verification involves two or more *models* of a device, where the models bear an uncheckable and possibly imperfect relation both to the intended design and to the actual device" — in a section she asks the reader to read even if the technical parts are skipped. cohn1989notion generalises the same material for a journal audience, held as a citation only. Then the choice itself, and it is worth reading as an argument rather than a progression. joyce1987hardware gives MOS devices **four** values -- Lo, Hi, Zz for high impedance, Er for error -- and an explicit abstraction function into boolean logic built on Hilbert's choice operator, so that what the abstraction does not cover is fixed but unknown and cannot be reasoned past. basin1989verification, two years later, writes the same device with the same identifier and **two** values, proving 5459 transistors against a model in which an undriven wire cannot be expressed; basin1991formally turns that model into verified synthesis. melham1993higher is the contemporaneous account of how abstraction levels get managed at all.

So the count of values in the model goes four, then two, then -- in Friedrichs, Függer and Lenzen -- back to three. That is not a tidy march toward fidelity, and the third step is not a return to the first: Joyce's Er is an error *value*, propagated compositionally, while metastability is not a value at all, which is precisely why mapping it to a fixed-but-unknown boolean does not work and why the 2018 paper needed a different construction.

**The routes across.** arora1993mosfet is the other bank — the compact MOSFET models simulation actually computes with — and reading it after Basin makes plain how much was thrown away. From there the members differ in which direction they move. Friedrichs, Függer and Lenzen *coarsen*: admit a third metastable value into a discrete model, propagate it worst-case, and buy deterministic containment by weakening what is modelled. yan2010formal *refines* to the limit, verifying an arbiter against a system of differential equations where the specification becomes topological constraints on trajectories and the obstacle stops being state-space size and becomes the stiffness of an integrator; it buys fidelity by weakening what is concluded, to almost-sure liveness — because the circuit is an arbiter and Marino forbids more. oulkaid2025modeles is the set's payoff and its only member that measures the trade: three transistor-level semantics, a switch one, a threshold one, and one on piecewise approximations of the I-V characteristics, compared on time, memory and soundness, with the finding that the semantics tracking SPICE most closely is the unsound one. kahng2011vlsi places the whole activity institutionally, defining electrical rule checking in one line as a routine sign-off gate. vetsch2025abinitio closes the set from below, with what it costs when no abstraction holds and the device must be simulated ab initio.

The shape worth carrying away: nobody escapes the gap, and the honest members say which side of it they are paying on. Coarsen and you keep determinism but model less; refine and you model more but conclude less.

Overlaps you-cannot-patch-silicon, which asks why hardware gets proved at all, and device-to-scaling-limit, which holds the physics. Neither asks this question. The distinction worth keeping: those two sets are about the economics and the substrate, this one is about the model in between, and a reader who conflates them will read Oulkaid's three semantics as three arbitrary implementation choices rather than as one abstraction and two successive repairs of it.