Do formal methods pay off?

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

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 set's oldest missing number arrived on 2026-10-17.** chen1996verification, written by the CMU and Intel people who did the work, states the Pentium FDIV cost in both currencies at once: "**About one trillion test vectors were used and none uncovered the bug. The recall and replacement of the chips in the field cost Intel $470 million.**" Every argument in this set about whether proof repays its cost has a counterfactual hiding in it, and this is the closest thing the corpus holds to that counterfactual being priced. Note what it prices: not the cost of verifying, but the cost of *not* having verified, which is the harder half and the one surveys omit. Its companion clarke1996word supplies the technique.

**Three measurements added on 2026-10-12, all from the proof-assistant line, and one of them does something none of the older members manage.**

andrici2020who **separates the cost of verification from the cost of the algorithm**, which is the distinction this set most needs and rarely gets. Its verified DPLL solver in Dafny is measured three ways: negligible overhead against the same algorithm written directly in C#; **roughly twice as slow as the same algorithm in C++**; and far behind MiniSat, which the authors attribute to CDCL being exponentially faster than DPLL rather than to any cost of proving. So verification costs about a factor of two and the algorithm choice costs everything else. The effort figures are equally plain: 3088 lines of Dafny including the parser, a **four-to-one ratio of proof to code**, written "in approximately one year and a half of part time work" by an author who learned Dafny during it. Its predecessor andrici2019verifying gave five to one and no such decomposition; quote the later one.

kurze2026nocout argues a different economy: **zero end-user verification cost**. Every network-on-chip its generator emits carries its own refinement proof, so the proof effort is spent once on the generator rather than per design -- the same argument puri2014using makes for certifying a transformation, and the reason both sit in derived-not-checked territory. Against that it reports a cost the set should note, because it is not an effort cost at all: the one-rule-at-a-time semantics that makes the proof tractable **serialises the routers in synthesised hardware**, so the abstraction is paid for in wall-clock time on the chip.

baty2024formal is the only member that prices verification in **regulatory** terms rather than engineer-months: interactive theorem provers have a very small trusted computing base, and for that reason "the French certification authorities for Common Criteria... recognize interactive theorem provers for the highest Evaluation Assurance Level". Where the rest of this set asks whether proof repays its cost to the builder, this one observes that a certifier may simply require it -- which changes the question from whether it pays to who is paying. 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". curzon1994formalb is the fullest measurement the set has, and the only one taken on hardware already in production: approximately two man-months to verify the 41 modules of the Fairisle ATM switching element, against a designer's estimate of several months to design it and several weeks to test it — so verification came to roughly what design and test cost together. It also measures what nobody else here does, the cost of *changing* a proof: after the specification was restructured, redoing proofs that had originally taken a month took under three days, because the lemmas were modular and the design was unchanged at the abstract level. And its result cuts against easy advocacy — no errors were found in the implementation at all, only in the specifications written about it, including the English commentary. lee2026formal is the first member to attack the cost rather than measure it: large language model agents wrote the large majority of its Rocq proofs, with the humans doing proof design and the agents the proof scripts, and the reported figures are a week for the core refinement and three weeks for the system inclusion on an out-of-order multiprocessor. If that holds up, the finding this set has carried since Cohn -- that it is the experts' time rather than computation time which makes verification expensive -- is the one being falsified, and the set should watch it rather than assume it. 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.

**The set's oldest answer is not a measurement at all but a demotion, and it arrived on 2026-09-17.** browne1986automatic -- Browne, Clarke, Dill and Mishra, IEEE Transactions on Computers, December 1986 -- ends by declining the claim its own method is usually sold on: "Verification is usually viewed as a way to guarantee correctness, and these techniques are no exception. However, we believe that these methods hold even more promise as debugging aids." The value they name is localising bugs and freeing designers from "the natural reluctance to modify a design that is already known to work". This matters to a set that mostly collects later people discovering the same thing at greater expense: the modest claim was the original claim, made by the method's inventors in its first industrial-strength application, and not a retreat forced on the field by disappointing trials. The paper earns its place by evidence as well as by assertion -- it finds a real timing bug in the published Seitz self-timed FIFO element -- and by the care with which it bounds what that evidence is worth: the bug is definite under the 3/2 design rules, and whether it would fail in silicon "depends on how accurately the 3/2 design rules model real circuits". A set about whether proof pays should keep one member that states plainly what a counterexample is a fact about.

**A co-design number arrived on 2026-09-17, and it is the sharpest cost comparison this set holds.** michelland2024lowlevel hardens RISC-V programs against a pipeline instruction-fetch attack using a small ISA extension plus a compile-and-link-time code transformation, with a security theorem that faults are detected by the end of every basic block. It costs a factor of **2.46 in code size** and **10.2 percent in execution time**. Against that it cites published software-only countermeasures on a secure boot program, of which only three combinations close more than 75 percent of vulnerabilities, all with "space overhead above x4.85 and time overhead above x5.01". **Roughly a fortyfold difference in time overhead, for a comparable class of attack, bought by touching the hardware.** Most members of this set price verification effort; this one prices where in the stack you place the defence, which is a question a design team actually decides.

Two qualifications belong with the number. The proof is **manual** -- the authors place their work among "manual proofs", not machine-checked ones -- and security is evaluated by emulated fault campaigns rather than on silicon. And the cost is a property of the program's shape, not a constant: long straight-line code pays least, loop-dense programs like dijkstra and bitcount pay most, and cryptographic routines do best "due to being computation-heavy with long blocks".

**SIX FIGURES ACQUIRED IN SEPTEMBER 2026, GATHERED HERE BECAUSE THEY ARE COMPARABLE AND THE SET'S OLDER MEMBERS ARE NOT.** Most of this set argues about whether proof repays effort in general. These price specific decisions, in units a design team recognises, and they are worth reading as one table.

- **A countermeasure with hardware support against one without.** michelland2024lowlevel: an ISA extension plus a code transformation costs **x2.46 code size and 10.2 percent runtime**; published software-only countermeasures closing more than 75 percent of the same vulnerabilities carry **space overhead above x4.85 and time overhead above x5.01**. Roughly a fortyfold difference in time, bought by touching the hardware. - **Turning the optimiser off to protect a countermeasure.** pesin2025formally: median runtime loss **87.99 percent** with countermeasures and no optimisation, **42.68 percent** with optimisation -- and optimisation demonstrably removes part of the protection. The choice is priced on both sides. - **Reusing an artefact you already own.** eslami2022reusing: compiling existing verification assertions into silicon as online Trojan monitors costs about **6.8 percent** in area, timing and power. The asset is free to obtain and not free to deploy. - **A completeness guarantee, by the hour.** neskovic2026sparc reports that the formal alternatives it declines cost **up to 35 hours per contract for Ibex, repeated after every hardware change**. That is what an absence proof costs when the design is still moving. - **Seeing information flow at all.** fan2026efficient: precise taint instrumentation grows a 136-thousand-cell design to **x5.81** and slows simulation **x143.72**; refining only where precision is needed brings those to about **x1.42 and x1.79**. - **And the cost of a design rule rather than a proof.** tarawneh2016formal: structural clock-domain-crossing checks on commercial systems-on-chip yield warnings "in the order of 100s of thousands of which **90 percent are false positives**", while a passing design still pays "the low throughput resulting from synchronization latency".

- **The cost of the expertise, priced as the binding constraint.** tan2025rtl reports a baseline that proves nothing in **seven days** where its own scheme proves every secure design, and proofs taking **2.5 to 45 hours** against attacks found in **under ten minutes** -- but its stated reason for choosing the formalism is human: writing shadow logic is "much closer to the standard activity of computer architects" than writing invariants, so the scheme "requires minimal formal-method expertise". The competing tool it measures against, LEAVE, automates the invariant search and still returns UNKNOWN after 2.1 hours on their small out-of-order core. **Two ways to spend the scarce thing: automate the expert, or pick a notation the non-expert already has.**

- **What the tools actually find, on a benchmark with ground truth.** ryan2023countering runs 84 properties against the Hack@DAC 2018 SoC (31 known bugs) and the OR1200 core (30) and finds **24 and 27**; on the same SoC, published figures for prior concolic execution are **14 of 31**, and the competition organisers report the commercial tools **Cadence SPV finding 6 and Cadence FPV 15**. All of its counterexamples were replayed in Vivado from reset. **A second, independent report of the same thing.** kande2022thehuzz investigated its own eleven found bugs with Cadence JasperGold and lists four reasons the tool did not serve: "state explosion, intensive resource consumption, reliance upon error-prone human expertise, and a requirement of prior knowledge of hardware vulnerabilities or security properties". Two unrelated groups, four years apart, reporting a commercial formal tool underperforming on open-core bug hunts -- **and note the fourth reason is not a defect but a definition:** a prover checks the property you give it. **A licence is not a result:** the money spent on a commercial formal tool bought, on this design, a fraction of the defects a research prototype found -- and this is the only ground-truthed comparison of that kind the corpus holds. The usual caution applies, that these are the authors' readings of others' reported numbers.

- **And a thirty-fold margin between two fault-verification tools.** tollec2024faultresistant proves 2-fault security of AES in **under 4 hours against 130 hours** for the prior tool FIVER, and then does 3-fault AES, which nobody had attempted. It reports no person-days at all, which is worth noting as an absence: the machine time is the part that got cheap, and this corpus's repeated finding is that the human time is the part that dominates.

- **Where the time actually goes, when someone measures instead of comparing.** ma2025bridging instruments a hardware fuzzing loop in an industrial flow and finds **over 90 percent of the performance loss is the verification environment, not the fuzzer**: coverage collection and mutation exceed 90 percent of total runtime with short seeds and stay above 50 percent as seeds grow, because simulators emit hierarchical coverage reports where a fuzzer needs a bit-vector. Replacing that one interface gives a several-hundred-fold speed-up in coverage collection and 12.7x on average end to end. **So most published fuzzing multiples are measurements of plumbing.** The same paper is the third independent citation in this corpus putting verification at about 60 percent of project effort -- stable across sources, and in every case cited from a survey rather than measured.

- **What the tools cannot do, priced in salaries.** coward2024rover, from Intel's numerical hardware group: "manual RTL design and optimization remains prevalent across the semiconductor industry because commercial logic and high-level synthesis tools are unable to match human designs" -- and their automated rewriting reaches **up to 63 percent circuit-area reduction** on Intel and open benchmarks at 5nm. **And the same group is trying to close that gap:** cheng2023seer reports up to **38x performance within 1.4x area**, an average of 2.9x, and an Intel case study where an automated search over rewrite orderings "demonstrates the potential to outperform manually optimized designs". Read the two together and the entry becomes a trajectory rather than a complaint: the 2024 paper prices what hand optimisation is worth, the 2023 paper measures how much of it a search can recover. **The cost being paid here is not the cost of proving; it is the cost of not having a tool good enough to trust**, paid continuously by engineers doing by hand what a specified compiler would do. tanaka2026relational prices the same gap as a fivefold performance swing on a syntactic rewrite, and mukherjee2016equivalence prices it as a functional bug in a shipped ARM FPU.

- - **A cost that fell, for once.** temel2020rprewriter proves 128-by-128 Wallace and Dadda multipliers correct in **27 to 39 seconds**, three times faster than the same rewriter without its fast-alist representation of the wire environment (83 and 101 seconds). **Industrial-width regular multipliers are no longer expensive to verify** -- which sharpens what drane2024systematic is really reporting when the truncated Booth variant defeats the method at 42 bits.

**And one member inverts the whole question.** drane2024systematic, from Intel: "the industrial adoption of truncated multipliers is limited by the absence of formal verification of such implementations, since exhaustive simulation is typically infeasible". **The proof is not a cost imposed on the design; it is the precondition for shipping a cheaper one** -- here a faithfully rounded truncated Booth multiplier, up to 31 percent smaller than externally truncated alternatives. Every other entry above prices verification as an expense; this prices its ABSENCE as a forgone saving. **And the proof runs out before the design does:** faithful rounding is verified to 42 bits and "runtimes grow exponentially, meaning we are unable to prove the correctness of the 64-bit truncated Booth multiplier".

- **One property, one protocol, fifty thousand proof obligations.** tan2025formalising proves single-writer-multiple-reader for a model of CXL.cache; SWMR is not inductive, so the strengthened invariant runs to **796 conjuncts across 68 transition rules** -- every conjunct proved preserved by every rule -- discharged by "dozens of sledgehammer calls simultaneously", each spawning "hundreds of automatic prover and SMT solver queries", with the invariant "revised many times". **And the model is two devices, one location, a reduced message set and a host with perfect tracking.** The proof was large enough to require new proof-engineering tooling, released as an Isabelle utility. **That is the current price of one coherence property on one industrial protocol.**

- **What the previous state of the art could reach.** ravi2024qed: hardware memory-consistency verification had been "limited to in-order-issue processors... or to bounded verification that does not scale in practice beyond **7 instructions across all threads**". **Seven instructions, for the property that decides whether a shared-memory multiprocessor means what its programmers think it means** -- a useful companion to the 796-conjunct invariant above, since the two measure the same difficulty from opposite ends: what a proof costs when it succeeds, and how far one gets before it stops.

- - **What a rank of error is worth, in area and power.** mrazek2025axmed: against "the well-optimized high-throughput implementation of the exact 9-input median, a **30 percent reduction in area and a 36 percent reduction in power consumption** was achieved by introducing an error by one position". **This set usually prices correctness as an expense; here inexactness is priced as a saving, with an exact analysis of how often and how badly the circuit errs rather than a simulation average.**

- **And its extreme form: verifiability as the fitness function.** ceska2020adaptive evolves approximate arithmetic circuits and checks each candidate with a SAT solver under a resource limit -- "if no decision is made within the limit, a minimal score is assigned to the candidate", so **circuits that cannot be verified quickly are selected out of the population**. The adaptive version raises the limit during the run so that slower-to-check but better circuits survive. It reports 32-bit approximate multipliers and MACs where prior methods "do still have a problem to scale above multipliers with 12-bit operands". **The bias is the point and also the caveat: the Pareto sets are of circuits that are good AND quickly checkable, which is not the same population.**

**And the same trade run the other way, deliberately.** wyse2025opensource designs a cache coherence protocol with **no transient states**, giving up request concurrency for simplicity, and model-checks it in CMurphi against a canonical MESI protocol: **up to 66x faster verification at 6 caches, where the canonical protocol at 8 caches would need an estimated 175 days.** Set beside drane2024systematic, where truncation and Booth encoding make a multiplier cheaper in area and unverifiable past 42 bits, the pair says what this set has been circling: **verifiability is a design objective competing with performance and area, not a property discovered afterwards** -- which is dhingra1987formal's argument, priced in a different currency forty years later.

**What the table shows that no single member does.** The expensive thing is rarely the proof. It is the **discipline the proof requires** -- registers inserted, optimisations forgone, monitors synthesised, instrumentation compiled in, synchronizers added, false alarms triaged. Several of these costs are paid whether or not anyone ever completes a proof, which is why a design team can experience formal methods as expensive while never having run a prover. **The set's question is better posed as: what does the discipline cost, and what would the same money buy elsewhere?**

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.