There are some computer programs that claim to check every step in a proof. However, various "soundness bugs" have been reported that at least potentially allowed false statements to slip past these programs. In many cases, these bugs have been demonstrated to be exploitable.
The list at the bottom of this page links to what appear to be reports of soundness bugs for various important proof-checking programs, sorted in increasing order of the number of reports. This list includes many more soundness bugs for these programs than the bugs mentioned in 2026 Paulson and 2026 StΓ©rin, and I don't think the list is missing any of the bugs mentioned there, but I've probably missed some reports. Please let me know about any corrections or additions.
Beware that this list doesn't include user-interface vulnerabilities. Those can have the same important effect of misleading a user as to what has been proven. See, e.g., 2016 Adams.
One standard path towards security is to minimize the complexity of the trusted computing base, which by definition is the part of the system that security reviewers need to check. From this perspective, HOL Light's proof-checking kernel is attractive because of its stability and simplicity, only 400 lines of code. But this size measurement doesn't say how carefully the HOL Light code has been reviewed, and doesn't say anything about the possibility of bugs in the underlying programming language.
Extra code can be good when it's test code. A battery of tests tends to catch more bugs than a single test. Running a proof through multiple proof-checking programs (preferably each in its own isolated environment) can save the day when there's a bug in one program, and is particularly easy if the checkers take the same input language for writing proofs. But it's not clear how effective this is at stopping attacks: for example, sometimes bugs are shared by multiple checkers.
The question "Who watches the provers?" is better answered by a proof saying that a checker works correctly. A close translation of the inference rules in the HOL Light kernel, except for the rules to introduce new definitions, was already proven in 2006 to generate only correct theorems. That proof was also checked by HOL Light. (For readers familiar with logic: of course this assumes a large cardinal; VΟ+Ο is enough for HOL Light. The same paper also has a variant of the proof that skips the large-cardinal assumption, at the expense of omitting the axiom of infinity from the logic being proven.)
After more work, a clone of HOL Light called Candle was proven in 2022 to allow only proofs of correct theorems, as long as the CPU implements the instructions used in the Candle binary in the expected way. This proof is again computer-checked, this time in another proof-checking system, HOL4. There was also a computer-checked proof in 2022 of the correctness of a standalone proof checker for HOL proofs in OpenTheory format.
From a security perspective, it's still concerning to be relying on large proof-checking binaries, where the answer to why we're supposed to trust one binary is that the binary has supposedly been checked by another large proof-checking binary. I'd like to see more work on simplifying these binaries.
The bug links below are accompanied by links labeled π to the Internet Archive Wayback Machine.
HOL Light (default usage, not Candle). Reported soundness bugs: 19960328π 20030718π 20030901π
Mizar (default usage, not mizar-rs). Reported soundness bugs: 20010625π 20030626π 20071226π 20230215π 20230227π 20230227-2π 20230227-3π
Metamath (default usage, not mmverify.py). Reported soundness bugs: 20171231π 20190211π 20190909π 20210621π 20230801π 20240708π 20250620π 20250727π 20251121π
Isabelle. Reported soundness bugs: 19930326π 19931122π 19950821π 19960627π 19991216π 20000708π 20030923π 20040823π 20060503π 20060512π 20140705π 20150824π 20161203π 20260116π 20260908π 20260910π 20261027π 20261105π
Lean (default usage, not nanoda; native_decide excluded). Reported soundness bugs: 20170124π 20171217π 20180409π 20210131π 20210308π 20220225π 20220806π 20221018π 20230127π 20230227π 20231010π 20250423π 20250524π 20260104π 20260301π 20260722π 20260725π 20260731π 20260731-2π 20260818π 20260818-2π 20260819π 20260819-2π 20260920π
HOL98/HOL4. Reported soundness bugs: 19990603π 20011205π 20011221π 20020305π 20020523π 20030113π 20030721π 20041025π 20050426π 20061011π 20090617π 20241014π 20260301π 20260301-2π 20260301-3π 20260314π 20260324π 20260722π 20260722-2π 20260722-3π 20260723π 20260723-2π 20260724π 20260728π 20260819π 20260819-2π 20261011π
Coq/Rocq. Reported soundness bugs: 19991208π 20010601π 20031028π 20070209π 20080514π 20081202π 20100210π 20100922π 20110726π 20111005π 20120209π 20131212π 20140115π 20140227π 20140410π 20150324π 20150630π 20150715π 20150906π 20150906-2π 20151122π 20160222π 20160519π 20160630π 20180131π 20180423π 20180526π 20180527π 20180604π 20180606π 20180828π 20181031π 20190102π 20190302π 20190406π 20190926π 20191015π 20191104π 20191123π 20191221π 20200118π 20200422π 20200603π 20200608π 20201109π 20201121π 20210219π 20210324π 20210513π 20211026π 20220321π 20220408π 20220530π 20221012π 20221012-2π 20221117π 20221117-2π 20221124π 20221207π 20230719π 20231213π 20240116π 20240206π 20240719π 20241121π 20250328π 20250403π 20250423π 20250423-2π 20250903π 20250903-2π 20260228π 20260228-2π 20260228-3π 20260302π 20260302-2π 20260302-3π 20260302-4π 20260302-5π 20260302-6π 20260302-7π 20260302-8π 20260310π 20260312π 20260321π 20260330π 20260428π 20260513π 20260513-2π 20260716π 20260818π 20260819π 20260820π 20260820-2π 20260820-3π 20260820-4π 20260820-5π 20260820-6π 20260820-7π 20260820-8π 20260820-9π 20260827π 20260909π 20260910π 20260919π 20261021π 20261025π 20261027π 20261027-2π 20261030π 20261104π
Version 20261112 of the "False computer-checked proofs" page.