By topic
A subject the papers are about. The loosest grouping, and the one to reach for last.
A
Absorbing a shock and recovering from one are different capabilities, and optimising for either misallocates against the other. Collects the works reaching that conclusion, in several fields that reached it independently. Membership requires the trade-off between the two to be the argument.
What computing does once the improvement everybody shared stops arriving. Collects the papers proposing where the next gains come from -- the layers above the device, specialised architectures, new models of computation -- and those arguing the gains are gone. It is a disagreement rather than a position, and members sort by the answer they give.
Whether a set of processes can agree on anything, and what has to be assumed before they can. Collects the consensus results, each a bound with conditions attached, and the impossibility results saying why the conditions cannot all be dropped. Membership requires the assumptions to be the subject: an algorithm that merely achieves agreement belongs elsewhere.
Answers to the aliasing problem given before there was a connective for it. Collects them in the order they were tried, from the observation that sharing is immaterial while nothing is updated onward. Membership requires the work to predate separation logic and to address aliasing directly.
Two nondeterminisms in one program: the demon resolves a choice against you, the angel in your favour. Collects the work treating a specification's freedom and an adversary's as one construct with opposite polarity. Membership requires both polarities to be in play; a calculus with only demonic choice belongs in the refinement sets.
Whether networks make democracy more participatory, asked under the same title twenty-six years apart. Collects the two framings together with the intervening work explaining why the answer changed. Membership requires the record to bear on that change rather than on participation generally.
Physical and microarchitectural attacks on what an instruction set never promised. Collects side channels in time and power, fault injection, speculative-execution leaks and memory-disturbance effects -- attacks on a correct implementation rather than on a flawed one. Membership requires the attack to exploit the hardware's behaviour, not a bug in the program running on it.
BGP believes what it is told, and a lie propagates as fast as the truth. Collects hijacks, leaks and the defences proposed against them, together with the protocol features that make them possible. Cases where the lever is the operator rather than the protocol belong here too, because from outside the effect is the same.
B
The layer the five-layer diagram draws as one box, where a shared medium has to be turned into orderly packets. Collects the medium access and framing work, from cable through bridged LANs to radio and satellite. Each change of medium forces a different answer, and membership turns on the medium's constraints being the subject.
C
'Is arithmetic consistent?' sounds like one question and is several: proved in what system, by what means, and answering to whose demand. Collects the consistency proofs and the arguments over what they establish, including works sharing a title that reach different answers. Membership requires the work to bear on what a consistency proof is worth, not merely to prove something about arithmetic.
Strategy's vocabulary applied to networks: key terrain, area denial, the gray zone, the kill chain. Collects doctrine, war-college writing and peer-reviewed research that make the borrowing, whatever their provenance. The recurring question is how much of each military concept survives the move, and record types here do not distinguish doctrine from scholarship -- readers must check.
D
Fifty years of asking whether the effort of proof repays its cost, and mostly answering no. Collects the software case studies, industrial audits and surveys from Fagan's code inspections onward, the definitional papers that fix what is being measured, and the same argument as mathematicians have had it about computer-assisted proof. Membership requires the work to argue about the payoff, not merely to apply a method.
The set's standing complaint about itself is that the papers which actually measure are outnumbered roughly five to one by the ones that survey. The hardware members are where that ratio is best, and they are worth reading as a group for it. Cohn's VIPER proof tabulates its own inference steps and CPU seconds and then says the tables are the wrong place to look — "it is the experts' time rather than computation time which makes verification expensive" — with a footnote giving the real figure: six months to organise and carry out the first of several levels. Basin and Del Vecchio price a single multiplexer at "approximately 45 minutes". Kumar and colleagues, surveying formal synthesis, price the one verified synthesis tool in their survey — a thousand lines of SML — at "about 8 man months", and conclude the approach does not scale to real tools. Oulkaid's thesis is the newest and the only one reporting adoption rather than promise, with the technique shipped in a commercial checker, and it publishes its own soundness gap rather than claiming it away.
The newest member is the one to watch. Guzman-Miranda and colleagues' 2025 VHDL methodology was commissioned by the European Space Agency under an activity called "lowering the adoption barriers for formal verification of ASIC and FPGA designs in the space sector" -- which is this set's question turned into a procurement line item. A funder paying to find out why its suppliers do not adopt formal methods is a different kind of evidence from a researcher arguing that they should.
Three independent groups across three decades, three orders of scale, and the same ratio of human time to machine time. That is a more useful answer than any of the surveys reach, and it is an answer the set can only give because it holds the works that counted.
Overlaps you-cannot-patch-silicon, where most of the hardware members also sit, and which asks why chips get proved at all rather than whether it paid.
F
The 1944 argument over the area bombing of German cities, conducted between people who agreed on the facts. Collects Vera Brittain's pamphlet -- held in its British edition, Seed of Chaos, while the American replies argue with the New York printing, Massacre by Bombing -- together with those replies, the postscript published alongside, a moral analysis in Theological Studies, a British airman's defence, and Zanetti's 1936 case for incendiary attack. The theme is what follows from evidence nobody contests, not what the evidence was.
The transistor, the integrated circuit, and the scaling rules that made each shrink pay for itself. Collects the founding device and process documents, Moore and Dennard, the papers arguing over where scaling stops, and the physical floors the shrink runs into. Most of its members are held as citations only, so the arguments are readable here and much of the primary record they argue over is not.
The set holds two floors, and they are different in kind. Landauer's is thermodynamic and quantitative -- erasing a bit costs at least kT ln 2, described in 1961 and measured fifty-one years later by Berut and others. Marino's is logical and qualitative: no physical implementation of a non-trivial digital circuit can deterministically avoid, resolve or detect metastability, so no bistable can be relied on to have settled. One says what computing costs; the other says what it cannot promise.
It also holds the modelling layer between the device and the circuit -- Arora's compact MOSFET models, which is what simulation actually computes with, and at the far end ab-initio quantum transport, which is what it costs when the compact abstraction stops holding. Those are the set's own statement of its limits, and the bridge to the-switch-or-the-curve, which asks the same question from the correctness side rather than the simulation side.
The post-CMOS candidates are here too -- tunnelling FETs, carbon nanotube FETs, ternary logic, cryogenic operation. Read them against gargini2017brief and the Moore retrospectives, which supply the industry's own record of how often a successor device has been announced.
H
How false claims move, and how much of the traffic they actually are. Collects the prevalence measurements and the diffusion studies that dispute what the averages mean. Membership requires an empirical claim about spread; arguments about why people believe belong in the sets on belief.
Fabrication: what has to happen physically before there is a chip to design for, from lithography and deposition through etch, process control and yield. Membership turns on the process rather than on the device it produces. Most members are technical video explainers rather than peer-reviewed work and the corpus's record types do not distinguish the two: they are reliable for mechanism and process order, and should not be cited for numbers.
I
Stated intention measured by survey, standing in for use that was never observed. Collects the technology-acceptance literature and the reviews criticising it on exactly that ground. Membership requires the gap between intention and use to be at issue.
L
File system design chasing a moving target: each layout is optimal for the hardware behaviour of its decade, and then the hardware changes. Collects the layout designs in sequence, so the argument between them is legible. Membership turns on the on-disk arrangement being the subject rather than the interface above it.
What a strand of glass or a waveguide on a die can be made to carry. Collects the optical-communication literature from Kao's 1966 loss argument onward, through the fibre systems that were actually built, to on-die photonic interconnect. The recurring disagreement is whether capacity comes from speed or from parallelism -- more wavelengths, more spatial paths -- and what integration cost each is worth.
M
Virtual memory as an idea about program behaviour: what a process will need next, and what it costs to guess wrong. Collects the papers making that argument, together with the retrospectives assessing it. Membership turns on the model of program behaviour, not on the addressing mechanism.
Arithmetic in the models that are not the intended one. Collects the three distinct ways of leaving the standard model -- initial segments, inconsistent models, and weakened induction -- rather than any single one. Membership requires the work to construct or characterise such a model, not merely to prove something independent of arithmetic.
Getting more than two states out of one device, and what that costs. Collects the multi-valued-logic designs together with the machine that tried it in 1959, so the modern circuits can be read against the one that was actually built and abandoned. Membership requires the work to implement or assess more states per device; a paper about the underlying material belongs in the fabrication sets instead.
The set now reaches up the stack as well as across the device. Setun is a working ternary computer; the CNTFET papers are ternary logic at the gate and circuit level; and Srinivasu and Sridharan's multi-digit adders are what you build once you have those gates -- the level where a radix change either pays or does not, because a ternary digit carries log2(3) bits and so needs fewer carry stages for the same range.
One caution for reading the modern members together. Setun's numbers are measurements of a machine that existed. Everything since is HSPICE simulation over compact device models, and the power-delay percentages are claims about a simulator rather than about silicon. Nothing in those papers misrepresents this, but the contrast with Setun is the most useful thing the set offers and it is easy to miss.
N
Networks whose nodes fly. Collects the work on aerial and swarm networking, where coverage and connectivity are the same trade-off seen from two ends: the further a swarm spreads, the worse its links get. Search-and-rescue deployments belong here as the application that forces the trade-off rather than as a separate subject.
O
Whether a chip's design and supply chain should be open. Collects the arguments from security, from verifiability and from economics, which reach different conclusions rather than agreeing. Membership requires the work to argue about openness itself, not merely to describe an open design.
Where the Internet came from, and what it was an answer to. Collects the founding network papers together with the alternatives they displaced -- air defence, the telephone system, the packet-switching proposals that lost -- because a choice reads as a choice only against what else was on offer. Histories written afterwards belong here alongside the papers they look back on.
One connective used in four directions: a postcondition that over-approximates what a program reaches proves bad states absent, and reversing the inclusion proves them present. Collects the program logics that vary which end is fixed -- Hoare, incorrectness, and the separation-logic variants of each. Membership requires the direction of approximation to be the point of the work.
P
Operating systems caught between speed and isolation, where every performance feature is a shared resource and every shared resource is a channel. Collects the work that treats that trade-off as the subject, from the capability and confinement papers of the 1960s to modern microarchitectural leakage. Membership requires the tension to be the argument, not an incidental cost.
Q
Quantum technology held between what has been demonstrated and what is claimed as a threat. Collects the deployment experiments, the cryptographic threat assessments and the migration guidance, so that the distance between them is visible. Membership requires the work to take a position on readiness or timing, not merely to concern quantum computing.
R
What a program logic can and cannot prove: completeness only relative to an assertion language rich enough to state the invariants. Collects the pursuit of that question from Turing's 1949 assertions through Cook's relative completeness to the higher-order logics where Cook's separation of assertion from specification no longer holds. Membership requires the work to bear on the completeness question itself, not merely to use a program logic.
Two ways of asking whether software is any good: run it to find errors, or count something and predict from it. Collects the testing literature and the software-metrics literature together, so the disagreement between them is visible. The recurring complaint is that the measures count size, which is what the set's earliest member says is the wrong thing to count.
S
Whether second-order logic is a foundation or set theory in disguise, and what its categoricity costs. Collects the foundational dispute and the results fixing the logic's expressive power. It reaches computing because separation logic's spatial conjunction is equivalent to second-order logic rather than a fragment of it.
Reasoning about the heap when pointers may alias. Collects the logic itself, its BI foundations, and the decidability and automation results that follow -- including the separating implication, where most of the difficulty lives. Works the logic argues with, such as Girard's linear logic, belong here as antecedents rather than as members of the tradition.
The Collatz conjecture, and what a field does with a problem it cannot close. Collects the responses -- computational verification, partial results, reformulation, and accounts of why the problem resists -- rather than the problem itself. Membership requires the work to be a response of a distinct kind, since the set exists to show that the responses differ in kind rather than in quality.
Verification by searching a program's states rather than deriving its properties. Collects the model-checking line from temporal logic through the algorithms and the tools that implement them. Membership requires the method to be exhaustive search over states; a deductive proof of the same property belongs in the program-logic sets.
T
Accounts of why a claim is believed that locate the answer in what the audience already held, not in the message. Collects the myth-layer, grievance-fitting and prior-belief explanations of persuasion. Membership requires the explanation to rest on the receiver rather than on the content or its delivery.
Where the Peano axioms came from. Collects the nineteenth-century originals the standard account names -- Grassmann, Frege, Dedekind, Peano -- in the language each was written in, with the notation sources they depend on. The set is a priority dispute, so membership requires the original text rather than a later exposition.
United States government documents that turn microelectronics assurance into a procurement requirement. Collects the assurance levels and the programme documents defining them. The levels are stated as adversary economics rather than defensive strength, and membership requires the document to set a requirement rather than analyse one.
The software supply chain after SolarWinds and Log4j. Collects the attack surveys, the guidance on judging dependencies, and the instruments that make such guidance binding. Membership requires the work to treat code you did not write as the exposure.
What happens to a network when the control plane is lifted out of the boxes that forward packets. Collects the argument that policy and mechanism were tangled, the architectures that separate them, and what a switch no longer has to keep once they are apart. Membership turns on the separation being the subject rather than an implementation detail.
Records whose held file is a different document from the work described. Collects both directions: a preprint, technical report or reprint standing in for the published version, and a whole volume or issue standing in for one item inside it. The criterion is physical and established by opening the file; the record's own page range against the copy's extent is what decides it.
Computing need not cost energy; erasing does. Collects Landauer's floor under discarding a bit, Bennett's reversible computation, the experimental measurement of the limit, and the work applying it to real machines. Membership turns on the thermodynamic cost of information, not on energy efficiency generally.
Claims that a computing system's damage appears where its own instrumentation cannot reach -- in attention, belief, working life and democratic process. Collects those claims and the arguments against them, including the case that the attribution is not new. Membership requires the harm to be argued as unmeasurable by the system causing it.
A language's designer giving their own account of how it came to be as it is. Collects first-person design retrospectives, chiefly from the History of Programming Languages conferences. Membership requires the author to have designed the thing described; a history written by anyone else belongs elsewhere.
Results published correctly, years before the work everyone credits. Held in pairs, so the earlier statement sits beside the one that travelled. The criterion is evidential rather than topical: the corpus must hold both documents, so the priority can be checked rather than asserted.
Why a formal apparatus invented for its own reasons should turn out to fit the world it is applied to. Collects the papers that take up Wigner's question directly, each answering the last and usually taking its title from it. Membership requires the work to argue about the fit itself, not merely to apply mathematics successfully.
One experiment on Facebook users and the notices its journal published afterwards. Collects the paper together with the editorial expression of concern and the correspondence about it. Nobody disputes that the manipulation worked; the set is about consent, and membership requires the work to bear on that dispute.
Readings of 5G that are not about radio. Collects the roadmap, the conspiracy theory tracked across a network, the adoption studies and the policy assessments together. Membership requires the work to treat 5G as a public argument rather than as a technology.
How many things a person can apprehend at once, and what sets the limit. Collects the numerical-discrimination and working-memory literature that pursues that single question, from Jevons in 1871 to the present. It is held in this corpus because the modern answer is a capacity argument of the kind applied elsewhere here to channels.
Second-order cybernetics: the move of putting the observer inside the system observed. Collects the papers that argue the position, the volume recording where it came from, and applications of it to particular systems. An application that denies the move applies -- as Fuchs does for the Internet -- belongs here as much as one that affirms it.
Algorithms published as algorithms, each held beside the paper that proves it correct. Collects such pairs so the program reasoned about can be read next to the reasoning. Membership requires the corpus to hold both halves; a proof whose algorithm is absent does not make a pair.
A key nobody stored: manufacturing variation measured on demand, so there is no secret at rest to read out. Collects physical unclonable functions and the attacks on them, from the optical and circuit-level founding papers onward. Membership turns on the secret being derived from physical variation rather than written into the device.
The 1968 Garmisch and 1969 Rome reports that named the software crisis, and the later accounts of them. Collects the primary conference records together with participants' retrospectives. Membership requires the work to be of or about those two meetings, not merely to discuss software engineering's difficulties.
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.
Systems in which a small disturbance is multiplied by the mechanism that makes the system work: feedback, convergence, replication, settlement. Collects cases from different fields that reach that conclusion independently. Membership requires the amplification to come from the working mechanism, not from a fault in it.
Transport, naming and encryption as they actually run rather than as the layer diagram draws them. Collects the measurements and retrospectives where a deployment diverges from its specification. Membership requires the gap between the two to be the finding.
Where trust in a running system comes from, when it cannot come from reading the source. Thompson's compiler attack is the origin; the rest is the industry discovering four decades later that he was describing a supply chain. Collects the attacks and the provenance, attestation and reproducible-build defences that answer them.
V
Proving a kernel's memory management correct, and what such a proof leaves out. Collects the machine-checked kernel verifications together with the memory models they must stand on. Membership requires the proof to reach memory management specifically; a verified component above it belongs elsewhere.
Proving things about code people actually run. Collects deductive verification applied to production Java, chiefly OpenJDK library code, together with the specification and tooling work it requires. Membership requires the target to be shipped code rather than an example written to be verified.
W
How much a channel can carry, and why noise is the limit. Shannon's 1948 paper is the subject; Nyquist and Hartley are here as the bounds that preceded it without a noise term, and the later work as what was built on it. Membership turns on the capacity of the channel itself, not on codes or protocols that use it.
What concurrent processes may share, and what keeps the sharing honest. Collects both halves of that question: the language constructs -- semaphores, monitors, message passing -- and the proof rules that track ownership of the same state. Membership requires the work to be about the sharing discipline itself, not merely to be concurrent.
Giving a program a meaning that is not whatever the implementation does. Collects the semantic traditions that each translate a program into something already understood -- a function, a logic, an abstract machine, an algebra, a type. What they disagree about is which of those may be assumed, and that disagreement is the set's subject.
What data is, asked as a live question in the years before the answer everyone now uses. Collects that exchange and its resolution, each paper answering the last by name. Membership requires the work to argue the definition rather than assume it.
The tools the proofs are actually done with: proof assistants, theorem provers, verification condition generators, decision procedures, and the libraries formalising logic itself. Every result in the other verification sets rests on one of these, and a tool built for one language belongs here as much as a general one. Membership requires the work to be about the tool rather than about a result obtained with it, and follows the tool through its renamings -- Coq and Rocq are one member of this set, not two.
A reading path for model checking, following section 6 of `halpern2001unusual` in the order the field built the results. Collects exactly the works that section cites, so the set is a bibliography of one survey section rather than of a subject. That section is titled *Automated verification of semiconductor designs*, which is worth knowing before reading it as a general history.
Attempts to say what the field is and what it protects. Collects the definitional papers, including those arguing that the standard triad is too narrow. Membership requires the work to argue about the definition rather than to apply one.
Countermeasures against an untrusted foundry that require nothing from it. Collects the techniques a designer can apply unilaterally -- locking, watermarking, obfuscation carried in the design itself. Membership requires the defence to need no foundry cooperation.
Accounts of what threatens critical infrastructure, from sources of different kinds -- agency advisory, think-tank survey, textbook, measurement study. They are grouped rather than reconciled, and the differences between them are the point. Membership requires the work to assert what the threat is, not to defend against one.
Arguments about fitting a hard subject into a curriculum, each naming what it gives up to do so. Collects the teaching positions -- which course, which logic, which half of the field is dropped -- rather than the material being taught. Membership requires the work to state the sacrifice, not merely to describe a syllabus.
Safety-critical systems: the accidents, the official responses, and the evidence about whether those responses were adopted. Collects the canonical cases together with awkward ones that resist the usual lesson, so a course cannot teach only the tidy examples. Membership requires software to be implicated in physical harm, not merely in loss or disruption.
Guarantees that were sound and failed anyway, because the failure arrived exactly where each one stopped. Collects the cases where a correct mechanism did not cover the fault that occurred. Membership requires the guarantee to have held on its own terms; a broken implementation belongs elsewhere.
Turning a design into geometry, where the wires and not the gates decide the outcome. Collects the physical-design literature: Rent's rule and the interconnect-delay results that establish why wiring does not shrink as logic does, and the placement, routing and packaging work that follows from it. Membership turns on the wires being the constraint, not on the design being physical.
Whether the guarantee that something works belongs inside the network or at its ends. Collects the two opposed positions -- the ARPANET subnet taking responsibility, CYCLADES refusing it -- the end-to-end argument that named the question, and what was built once it was settled. Also holds the works that test the answer on its own terms, where no end-to-end path exists or the thin waist has a cost.
Designs for a logic settled by naming who will use it -- a machine, a student, an engineer. Collects the papers that justify a logic's shape by its intended user. Membership requires the user to be the stated reason for a design choice.
Works whose own copy names a defence or nuclear funder -- Project MAC, ARPA and DARPA, ONR, AFOSR, the Air Force laboratories, Army Ordnance, the Atomic Energy Commission. The criterion is physical: the line must be printed on a title page, in a footnote or in an acknowledgement in the copy the corpus holds. It appears in no catalogue record, so every member was established by someone opening the file and reading it.
Measurement rather than attack: where the traffic actually goes, and how few places carry it. Collects studies of internet exchange points, route servers, transit concentration and the physical and organisational chokepoints traffic passes through. The theme is structural fragility established by measurement; works arguing an adversary's capability belong in the attack sets instead.
How two parties who have never met agree a key and learn whom they are talking to. Collects the authentication protocols, the attacks that found them broken years after publication, and the logics proposed to settle such questions. The theme is that these protocols fail quietly: membership requires the work to bear on whether a protocol is correct, not merely to specify one.
Arguments for a way of programming, as against accounts of what a program means. Collects the position papers that tell you how to write, structure or decompose programs and why. Membership requires a prescription: a semantics or a proof method belongs in the sets about meaning instead.
Y
Proving a chip correct before it is built, because a fabricated error cannot be patched. Collects hardware verification work whose argument rests on that asymmetry -- the economics of verification differ from software because a respin costs a fabrication run. Membership turns on the irreversibility premise, not on the method used.
The set used to run 1977, 1986, and then jump to 1993 and on to the industrial reports from 1999. That gap held the field's founding decade, and it is now filled. The three cases everyone treats as the beginning are here: Cohn's machine-checked proof of the VIPER microprocessor at Cambridge in HOL, Hunt's FM8501 at Texas in the Boyer-Moore logic, and Barrett's formalisation of IEEE 754 at Oxford in Z, which INMOS used in building the T800's floating-point unit. Three countries, three logics, three institutions, within about five years. Beside them sit Basin's two Cornell papers, which are the switch-level end of the same decade, and Kumar and colleagues' 1996 survey, which is where the period got classified.
Cohn's two Cambridge reports are the ones to read first, and Section 2 of the second -- which she asks the reader to read even if the technical sections are skipped -- is the best statement in the set of what the whole activity can and cannot establish. Joyce's dissertation is the constructive reply: a specification discipline whose stated purpose is "a sharp distinction between what has and what has not been formally considered in a proof of correctness".
Read the founding cases for their caveats rather than their results, because the caveats are better than the reputation of the field suggests. Cohn in 1987 warns in her own conclusions against "a false sense of security afforded by an HOL proof" on the grounds that "there are many classes of errors not even visible in the models used", and records that the errors she found in VIPER's specification "are apparently not present in the actual chip; hence the manufacturers cannot have used the specification which we have started to verify". The set's sceptical voice is its earliest one, not a later correction.
The set does not stop in 1996. Guzman-Miranda and colleagues' 2025 methodology for formally verifying VHDL designs was funded by the European Space Agency under a programme whose stated aim is "lowering the adoption barriers for formal verification of ASIC and FPGA designs in the space sector" -- the irreversibility premise at its most literal, since a part in orbit cannot be recalled at all.
Costs, where members report them, are consistent across the whole span and are always in human time rather than machine time: 45 minutes for one multiplexer, six months for the first of several levels of one microprocessor, eight man-months for a thousand lines of a synthesis tool. Cohn states the general form of it -- "it is the experts' time rather than computation time which makes verification expensive".
Overlaps do-formal-methods-pay, which asks whether any of this repaid the effort, and the-switch-or-the-curve, which asks the narrower question of how much of the device a correctness argument admits in the first place.