A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once through a case split on whether the always-diverging program bot satisfies the property in question. We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP): valid in intuitionistic logic, requiring neither diagonalization nor self-reference, and adding no classical reasoning beyond the MRDP assumption itself. The key idea is a two-witness construction. Given a non-trivial property P, we attach to each Diophantine polynomial D a pair of programs S^0_D, S^1_D that behave like the negative and positive witnesses for P when D is solvable, and both diverge identically when it is not. A hypothetical decider for P would therefore decide Diophantine solvability via the difference delta_D = DecideP(S^1_D) - DecideP(S^0_D) -- contradicting the MRDP theorem. The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot). The undecidability of the halting problem follows as an immediate corollary: a single application of Rice's theorem to the Terminates property. A formalization in the Rocq proof assistant confirms both results within a step-indexed model of computation, with the undecidability of Hilbert's Tenth Problem as the sole external axiom. Both Rice_Theorem and Halting_Problem are closed under the global context.
Comments: 46 pages, Rocq (Coq 8.18+) formalization included. Source and C witness: endrazine/rice-constructive
Seven CVEs for Theorem Provers That Accept False Proofs: Jonathan Brossard and Jean-Philippe Aumasson at [un]prompted 2026
Soundness bugs in the theorem provers Lean and Rocq let a crafted input make the tool accept a proof of a false statement, and the speakers obtained seven CVEs for them.
A theorem prover is software that mechanically checks a mathematical proof, where Rocq is the renamed Coq. Soundness is the property that it cannot accept a proof of something false, so a soundness bug breaks the one guarantee the tool exists to provide.
Those bugs have always existed, while the stakes changed with vericoding, the practice of having AI generate code together with a machine-checked proof that the code is correct. If the checker can be fooled, the proof stops being evidence.
The speakers exploit the bugs to forge short proofs of famous open problems, including P = NP along with the Riemann Hypothesis, deliberately crude enough that an expert would not be fooled, while noting more convincing forgeries are possible.
In their [un]prompted 2026 talk, "Hacking Truth: Forged Lean Proofs and the Risk of Verifier Bugs," on Thursday, October 29 at 9:35 a.m. on Stage 2, Jonathan Brossard and Jean-Philippe Aumasson argue that provers should be treated as security boundaries.
Speakers:
- Jonathan Brossard, psirt.com (presenter)
- Jean-Philippe Aumasson, Cryptography Team Lead, Cloudflare (presenter)
A second result reaches into production cryptography. The speakers sabotage a Fiat-Crypto field multiplier so it always returns zero while its original correctness theorem still verifies, which matters because Fiat-Crypto generates formally verified arithmetic used by BoringSSL. They also demonstrate soundness failures in Z3, an SMT solver that many verification tools trust.
Two of the seven CVEs are in the public record. Brossard posted an oss-security advisory for a Lean 4 kernel bug that forges proofs via nested inductive projections, rated 7.1, with a Docker proof of concept.
CVE-2026-72703 covers a Rocq guard-checker flaw that accepts non-terminating fixpoints, allowing a proof of False. The bug class became public when an AI-assisted Lean project claimed a disproof of the Collatz conjecture in July 2026.
Jonathan Brossard, known as endrazine, is a French hacker along with a computer science professor at the Conservatoire National des Arts et Métiers. He presented Rakshasa at Black Hat USA 2012, a proof-of-concept hardware backdoor in BIOS and PCI firmware. He is also the main author of the Witchcraft Compiler Collection.
At DEF CON 34 in 2026 he announced his acquisition of the Bugtraq name, relaunching the full-disclosure mailing list.
Jean-Philippe Aumasson leads cryptography at Cloudflare. He co-designed the BLAKE2 and BLAKE3 hash functions along with SipHash. He also co-designed SPHINCS+, standardized by NIST as SLH-DSA, together with Argon2.
He wrote Serious Cryptography along with Crypto Dictionary, and he gave a zkStudyClub talk surveying real bugs found in zero-knowledge proof systems.
To go deeper on the topic, start here:
- Jonathan Brossard's oss-security advisory on the Lean 4 kernel soundness bug
- CVE-2026-72703: Rocq guard checker accepts non-terminating fixpoints, proving False
- Docker proof of concept for the Lean kernel soundness bug
- Proof of concept for the Rocq soundness issue
- Lean 4 issue 14576 and its fix
- BoringSSL's vendored Fiat-Crypto field arithmetic
Anyone relying on machine-checked proofs, especially for verified cryptographic code, gets a reason to treat the checker as attack surface.
If a proof is only as trustworthy as the verifier, when did you last check your verifier for soundness bugs?
2 points · 1 comment
Mentions
A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once through a case split on whether the always-diverging program bot satisfies the property in question. We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP): valid in intuitionistic logic, requiring neither diagonalization nor self-reference, and adding no classical reasoning beyond the MRDP assumption itself. The key idea is a two-witness construction. Given a non-trivial property P, we attach to each Diophantine polynomial D a pair of programs S^0_D, S^1_D that behave like the negative and positive witnesses for P when D is solvable, and both diverge identically when it is not. A hypothetical decider for P would therefore decide Diophantine solvability via the difference delta_D = DecideP(S^1_D) - DecideP(S^0_D) -- contradicting the MRDP theorem. The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot). The undecidability of the halting problem follows as an immediate corollary: a single application of Rice's theorem to the Terminates property. A formalization in the Rocq proof assistant confirms both results within a step-indexed model of computation, with the undecidability of Hilbert's Tenth Problem as the sole external axiom. Both Rice_Theorem and Halting_Problem are closed under the global context. Comments: 46 pages, Rocq (Coq 8.18+) formalization included. Source and C witness: endrazine/rice-constructive
Seven CVEs for Theorem Provers That Accept False Proofs: Jonathan Brossard and Jean-Philippe Aumasson at [un]prompted 2026 Soundness bugs in the theorem provers Lean and Rocq let a crafted input make the tool accept a proof of a false statement, and the speakers obtained seven CVEs for them. A theorem prover is software that mechanically checks a mathematical proof, where Rocq is the renamed Coq. Soundness is the property that it cannot accept a proof of something false, so a soundness bug breaks the one guarantee the tool exists to provide. Those bugs have always existed, while the stakes changed with vericoding, the practice of having AI generate code together with a machine-checked proof that the code is correct. If the checker can be fooled, the proof stops being evidence. The speakers exploit the bugs to forge short proofs of famous open problems, including P = NP along with the Riemann Hypothesis, deliberately crude enough that an expert would not be fooled, while noting more convincing forgeries are possible. In their [un]prompted 2026 talk, "Hacking Truth: Forged Lean Proofs and the Risk of Verifier Bugs," on Thursday, October 29 at 9:35 a.m. on Stage 2, Jonathan Brossard and Jean-Philippe Aumasson argue that provers should be treated as security boundaries. Speakers: - Jonathan Brossard, psirt.com (presenter) - Jean-Philippe Aumasson, Cryptography Team Lead, Cloudflare (presenter) A second result reaches into production cryptography. The speakers sabotage a Fiat-Crypto field multiplier so it always returns zero while its original correctness theorem still verifies, which matters because Fiat-Crypto generates formally verified arithmetic used by BoringSSL. They also demonstrate soundness failures in Z3, an SMT solver that many verification tools trust. Two of the seven CVEs are in the public record. Brossard posted an oss-security advisory for a Lean 4 kernel bug that forges proofs via nested inductive projections, rated 7.1, with a Docker proof of concept. CVE-2026-72703 covers a Rocq guard-checker flaw that accepts non-terminating fixpoints, allowing a proof of False. The bug class became public when an AI-assisted Lean project claimed a disproof of the Collatz conjecture in July 2026. Jonathan Brossard, known as endrazine, is a French hacker along with a computer science professor at the Conservatoire National des Arts et Métiers. He presented Rakshasa at Black Hat USA 2012, a proof-of-concept hardware backdoor in BIOS and PCI firmware. He is also the main author of the Witchcraft Compiler Collection. At DEF CON 34 in 2026 he announced his acquisition of the Bugtraq name, relaunching the full-disclosure mailing list. Jean-Philippe Aumasson leads cryptography at Cloudflare. He co-designed the BLAKE2 and BLAKE3 hash functions along with SipHash. He also co-designed SPHINCS+, standardized by NIST as SLH-DSA, together with Argon2. He wrote Serious Cryptography along with Crypto Dictionary, and he gave a zkStudyClub talk surveying real bugs found in zero-knowledge proof systems. To go deeper on the topic, start here: - Jonathan Brossard's oss-security advisory on the Lean 4 kernel soundness bug - CVE-2026-72703: Rocq guard checker accepts non-terminating fixpoints, proving False - Docker proof of concept for the Lean kernel soundness bug - Proof of concept for the Rocq soundness issue - Lean 4 issue 14576 and its fix - BoringSSL's vendored Fiat-Crypto field arithmetic Anyone relying on machine-checked proofs, especially for verified cryptographic code, gets a reason to treat the checker as attack surface. If a proof is only as trustworthy as the verifier, when did you last check your verifier for soundness bugs?