I’m trying to assemble a clear, expert-level answer to a common worry: Even if Coq’s kernel is correct, how can a proof still “pass” in Coq and yet be logically unsound? I’m looking for a canonical breakdown of failure modes, concrete examples, and best-practice mitigations.
Specific questions:
What are the main ways Coq can accept a “proof” that is mathematically wrong without a kernel bug?
Which real-world examples best illustrate each class of failure?
What checks or workflows catch these issues in practice (e.g., CI, Print Assumptions, audit scripts)?
How should one reason about the Trusted Computing Base (TCB) when using external tactics, plugins, or fast evaluators?
What are the recommended defaults (flags, styles, policies) to minimize risk?
What I’ve gathered so far:
Unsound or incompatible axioms.
Coq accepts axioms at face value; an inconsistent axiom (or inconsistent combination) lets you derive anything.
Mixing libraries that quietly assume conflicting axioms (e.g., certain forms of choice, K, univalence, classical axioms) can render the environment inconsistent.
Mitigation: avoid unnecessary axioms; isolate classical vs constructive parts; always run Print Assumptions theorem_name.
Admits and “cheats” disguised as proofs.
Admitted (or equivalent tricks) turns a goal into an assumption; theorems depending on it “prove” nothing.
Historically, workarounds (custom todo axioms, unsafe tactics) could let Qed finish with hidden holes. The coloured theorem is the opposite of this, right?
Mitigation: forbid Admitted/cheat tactics in release builds; grep for them; enforce “no-axioms/no-admits” CI checks.
Opaque proofs masking dependencies.
Qed hides the proof term; you can unknowingly depend on a strong axiom or a lemma with Admitted.
Mitigation: use Print Assumptions; make critical proofs Defined during review; keep a “no-opacification until audit” policy.
Tactic/engine misuse and unsafe primitives.
Some low-level commands (historically, “no-check” variants) can change goals unsafely; poorly constrained metaprogramming can produce bogus terms.
Fast evaluators (vm_compute, native_compute) and backtracking interactions have had soundness bugs in the past.
Human mis-specification / proving the wrong statement.
Common pitfalls: hidden section variables, missing generalization before induction, or proving a conditional you didn’t intend.
Mitigation: inspect final statements (Check/Print); require explicit quantification/generalization patterns in reviews.
Trusted plugins and external oracles.
Plugins that don’t produce checkable proof terms—or trust external computations—expand the TCB. Bugs here can certify false theorems.
Mitigation: prefer certificate-producing tools (e.g., SMT with proof objects) and verified pipelines; audit plugin assumptions.
Historical examples (non-exhaustive):
A classic “fast reduction” exploit (very large inductive type + evaluator) produced a proof of False without explicit axioms.
Incompatible axiom stacks across libraries leading to trivialization.
AI-generated proofs using “cheat” tactics (admit/sorry analogues) that pass unless filtered.
Operational safeguards I’ve seen recommended:
CI checks that fail on: (a) any Admitted, (b) any axioms outside an allowlist, (c) Print Assumptions non-empty for public theorems.
Pin Coq + plugin versions; maintain a “soundness watchlist” of features (primitive projections, universes, native/vm compute).
Enforce review checklists: final statement match, explicit binders, no unintended section deps, no hidden classical assumptions.
What I’d appreciate from the community:
A vetted taxonomy with pointers to canonical docs/posts.
Minimal repro scripts for key pitfalls (axiom clashes, “wrong theorem” via bad generalization, evaluator gotchas).
A concise “hardened Coq” checklist (flags, lints, CI patterns, allowed plugins).
Any updates on modern best practices for integrating external solvers safely (proof certificates, checker maturity).
Context:
This question consolidates discussions I’ve seen in papers, issue trackers, and forum threads, plus anecdotes from competitions where AI systems sometimes slipped in admits/cheats. I’m hoping to turn this into a reference answer others can point to when onboarding contributors or designing CI for large Coq projects.
Print Assumptions can get confused in presence of modules. The safer bet is to run coqchk.
Unsafe tactics have never let Qed accept a broken proof. As for custom todo axioms, they are no different from standard axioms; the kernel will happily accept them as long as their application is correctly typed. As for the “colored theorem”, I have no idea what you are referring to.
Using Defined instead of Qed does not change anything in that regard. Indeed, Qed does not hide the proof term, it just abstracts it away, preventing it from participating to computations. You can still look at it with Print.
Bogus terms (which include goals changed unsafely) will not pass the kernel check, if the latter is correct. More generally, tactics have never been part of the trusted computing base. They can contain bugs, as long as they do not corrupt memory.
Unfortunately, it so happens that, as a user, you can corrupt the memory of Rocq, at which points all bets are off. I am not sure how to mitigate this kind of attack.
vm_compute and native_compute are part of the trusted kernel and hence are as correct as the kernel. So, you are moving the goalpost here. It is no longer “How can Coq accept an unsound proof if the kernel is correct?” But it becomes “Is there some small set of features that have a higher chance of being correct?” For example, modules have had a large share of bugs. By the way, regarding vm_compute and native_compute, most of the bugs were not with them specifically but rather with primitive types.
You are conflating “no proof” and “unsound proof” here. A plugin cannot produce an unsound proof in general. It can, however, generate axioms. So, again, mitigations like Print Assumptions and coqchk apply.
I’m not sure how much corruption we’re talking about here, but if there is a way to semantically separate the memory the plugin has write access to from the kernel memory, it should be possible to run the Rocq process with a privileged user on a CHERI capable CPU. This would prevent unprivileged processes on the same OS to modify the kernel memory (for example running as root if the user processes are not trusted) and it would prevent the plugin to modify the kernel memory by having the kernel only provide read-only capabilities for the parts of the kernel memory the plugin needs to read (and providing full capabilities for the parts of the memory the plugin should own). Plugins can only modify kernel memory by calling kernel functions.
Note that I did not use the word plugin in that part of my post. (Said otherwise, you do not even need a plugin to trigger the corruption.) The issue is that, if you feed a sufficiently strange term to the pretyper (the untrusted part of Rocq that is responsible for inferring all the data needed by the kernel), then you can get it to behave undefinedly. So, it is not just the plugins that you need to defend the kernel against, but all the other parts of Rocq.
Note that I do not know if you could skip the pretyping stage and directly feed a strange term to the kernel and/or coqchk. If they were to behave as badly as the pretyper (they share a lot of code, so this is likely), then protecting the kernel memory would not be enough. Some more radical changes would be needed.
By the last “it” do you refer to “the kernel”? Because if it refers to “the pretyper” then I’m not sure the pretyper should be considered untrusted.
My (naive) expectations would be that only trusted components need to behave as specified in order for the whole execution (from the initial file to the final output) to behave as specified: successful outputs are sound. Untrusted components can make a statement fail to be proven or the whole execution to fail (e.g. insufficient resources), but they cannot make a statement be proven if it is not provable in the theory.
Do you mean that tactics (which are untrusted components) can abuse the pretyper to corrupt the kernel state (without the kernel noticing) and make a theoretically unprovable statement practically provable?
I’m assuming this doesn’t hold under adverserial conditions like another process messing up with /proc/PID/mem or a plugin messing up with /proc/self/mem or Obj.magic.
>Do you mean that tactics (which are untrusted components) can abuse the pretyper to corrupt the kernel state (without the kernel noticing) and make a theoretically unprovable statement practically provable?
yes, as mentioned the kernel does not protect its memory
Yes, I am referring to the pretyper. And why would it have to be trusted? Its only purpose is to fill holes that the user was too lazy to fill. Obviously, without a pretyper (aka elaborator), a proof system would be unusable. But it is not involved at any point in the checking of a proof.
Let us be clear. Once there is a memory corruption (e.g., buffer overflow), all bets are off, whatever the kind of software. The ability to check an unprovable statement should be the least of your worries. You should be more concerned about your computer catching fire and burning down your house. This is an actual safety bug in Rocq, which needs to be fixed at some point.
Back to the original topic, as Freek Wiedjik explained (it was a long time ago, so I might be getting the points a bit off), there are three points to keep in mind when looking at a formal proof:
What does it even mean that a formal proof is correct and/or accepted by the kernell? (My own take on this is the case of some defective hardware or some stray cosmic ray. But the question is much more philosophical and has to do with our beliefs.)
The kernel is a piece of software and every piece of software has bugs. Do not trust people who tell you otherwise. (The above corruption issue is such an example.)
The kernel only checks the proofs; it is the human who is responsible for the statements.
Because I define “trusted components” as the parts of a whole for which it is sufficient to assume some properties such that the whole satisfies some properties. With this definition, “trusted component” is not a binary concept, a component is more or less trusted depending on the strength of the properties we assume of it.
When you say “then you can get [the pretyper] to behave undefinedly”, it suggests you expect some properties of the pretyper (to behave definedly). Those properties may be much weaker than some canonical property you may have in mind when I say it should be trusted (like correctness). But in the end, to trust Rocq, one needs to trust that the pretyper satisfies those trivial properties, even if it’s only a very weak level of trust.
Maybe those trivial properties are satisfied by assuming a stronger property on a different component (like the programming language). To trust a program, you have multiple options:
Trust the programming language to behave according to its specification regardless of some if its possibly implicit environmental requirements. This is a strong (and unrealistic but convenient) level of trust.
Trust the programming language to behave according to its specification and recursively trust its environmental requirements (for example that the OS, VM, and/or CPU behave as required by the PL). In theory one can recursively extend the trust base possibly down to the assumed rules of the universe (which has no requirements), each time choosing the weakest level of trust for each component.
Even though in both cases we trust the PL, we don’t trust it in the same way. I suspect that’s the same issue with the pretyper. I say it’s trusted and you don’t, but it’s just a matter of the properties we need to assume of it.
We are not using “trusted” with the same meaning. I am using “trusted” as in “trusted computing base” (TCB), which has a very clear meaning that does not leave much to personal interpretation. And it is a binary concept: Either a component is in the TCB or it is not. In the case of the pretyper (same for tactics), it is theoretically not part of the TCB of Rocq, since the ability of the kernel to check a given kernel term should not depend on what the pretyper is doing. Unfortunately, because the pretyper and the kernel share the same memory space, a buffer overflow in the pretyper can corrupt the memory of the kernel. So, while the pretyper is not part of the TCB in theory, one cannot completely excludes it in practice.
As for “behaving definedly”, it means not having any undefined behavior, which is the absolutely strict minimum you can expect from a piece of software. Safety bugs, by definition, break this assumption.
I don’t think TCB is relevant for this issue (unsound proof accepted by trusted kernel). TCB is just an instantiation of my definition of trusted where the properties of the whole are about security only, not any form of correctness.
TCB is not just about security. It has a widely accepted meaning in the domain of theorem provers. Here are a few examples of its use, but I am sure you can find a lot more of them:
Appel et al, “A Trustworthy Proof Checker”: “the TCB consists of two pieces: first, the specification of the safety predicate in higher-order logic, and second, the proof checker, a small C program that checks proofs, loads, and executes safe programs.”
Avigad & Harrison, “Formally Verified Mathematics”: " This was the method used by Gonthier in the verification of the four-color theorem in Coq; because it is based on a constructive logic, Coq‘s “trusted computing base” is able to normalize terms and thereby carry out a computation."
Baty, " Formal Specification and Verification of Security Mechanisms for RISC-V Processors": “Proof assistants have a limited Trusted Computing Base (TCB) compared with the more specialized tools found in the industry, making them more trustable”
Boulmé & Monniaux, “The Trusted Computing Base of the CompCert Verified Compiler”
Even Pollack’s 1997 paper was already using “trusted” with the above meaning (though he did not use the whole expression “trusted computing base” at the time).