You cannot patch silicon
A subject the papers are about. The loosest grouping, and the one to reach for last.
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.