Tagewerk XVI
Independent Coq (Rocq 9.0) + Isabelle2025 re-decision for verification-amplification (ADR 0048)
A new faculty for the daemon: independent re-decision of a proof in a SECOND and THIRD kernel. Leibniz's proof edge had one arbiter, the Lean 4.31 kernel. This cycle adds report-only backends for the Rocq 9.0 (Coq) and Isabelle2025 kernels, so a published result can be re-decided in a different trusted core — strictly stronger evidence than re-running the same one, because an independent kernel catches translation and kernel-specific errors a single-checker pipeline cannot. Both are LIVE for verification-amplification (audit tier) and DORMANT for promulgation: they never write kernel_verified, mint no proof edge, and — until an operator admits their producer strings under the ADR 0041/0045 allowlist ritual — the trust policy rejects any Coq/Isabelle proof edge structurally, so the trust boundary is unchanged (all four structural guards stay byte-identical). The backends genuinely GATE, not rubber-stamp: on the demo certificates each kernel accepts real theorems (Coq's add_comm / app_assoc / rev_involutive; Isabelle's add_comm / rev_rev / Gauss's summation) and REJECTS both self-laundered proofs (Coq `Admitted`; Isabelle `sorry`) and broken proofs. A three-round adversarial review (six false-PASS holes found and closed, each pinned as a regression test) drew a hard, honest line between the two kernels' trust. For Coq the axiom audit is KERNEL-DRIVEN AND SOUND: after compiling, the backend runs Rocq's own library checker `rocqchk`, which reports the whole development's axioms and unsafe constructs name-agnostically, with the authentic verdict fenced off by an unforgeable random nonce the compiled source cannot read; a final 25-attack validation could not certify a single proof of False. For Isabelle, which exposes no such report reachable without ML, the check is a comprehensive source blocklist that is NOT adversarially sound (each review round found a fresh route: a cheat tactic, then a setup-ML axiom injection, then a code_printing + eval); it is therefore scoped to trusted-provenance amplification only, with a kernel proof-term audit recorded as the blocking prerequisite for any Isabelle promotion. LLMs propose nothing here; the kernels decide, and the daemon reports what they said.
Verdicts — machine-adjudicated (5)
- DELIVERED capability Independent Coq (Rocq 9.0) + Isabelle2025 re-decision, report-only
leibniz/backends/coq_docker.py + isabelle_docker.py, built to the lean_cli contract; they only REPORT the kernel verdict. Coq amd64-under-Rosetta; Isabelle native arm64. No trust surface: trust.py / verifiers.py / test_invariants.py / the two write-guard tests are byte-identical.
- CERTIFIED gate Both kernels gate on the demo certificates (accept real, reject laundered/broken)
Coq: add_comm, app_assoc, rev_involutive verified (rocqchk: axioms <none>); `Admitted` and a false goal rejected. Isabelle: add_comm, rev_rev, Gauss's summation built; `sorry` (hard error at quick_and_dirty=false) and a false goal rejected. scripts/verify_multi_kernel.py — gate GREEN.
- CERTIFIED coq-sound The Coq axiom/unsafe audit is kernel-driven and sound
`rocqchk -o` re-validates the compiled .vo and reports the whole development's axioms + type-in-type / unsafe-(co)fixpoint / assumed-positivity name-agnostically; an unforgeable nonce authenticates the verdict against source output-injection. A 25-attack adversarial validation found no false PASS (no proof of False, no hidden axiom, no forged summary).
- NOTED isabelle-scope The Isabelle check is best-effort, NOT adversarially sound
No rocqchk-equivalent is reachable without ML, so the backend is a comprehensive source blocklist; three review rounds each found a fresh laundering route. Scoped to trusted-provenance amplification only; a kernel proof-term audit (Thm_Deps.thm_oracles + axiom deps from a wrapper theory) is the blocking prerequisite for Isabelle promotion (ADR 0048 §2/§4.2, HANDOFF ticket).
- NOTED promotion Promotion to a proof-edge decider is deferred and operator-gated
The CoqVerifier/IsabelleVerifier + registry that would write kernel_verified are NOT landed — prototyping them tripped the structural trust guards. The KERNEL_PRODUCER→KERNEL_PRODUCERS edit + guard-whitelist edits are an operator keystone, gated per the ADR 0045 8/8 proof-edge deferral.
Re-runnable artifacts
- coq_demo.v ↓ sha256 f0dcac86b7c7…
- isabelle_demo.thy ↓ sha256 10213a6812ee…
Files download verbatim from this site — the exact kernel-checked bytes (verify the SHA-256). See how to re-verify.
Repositories — the code trail
- produced elementalcollision/leibniz-daemon #297 ADR 0048: leibniz/backends/{coq_docker,isabelle_docker}.py + scripts/verify_multi_kernel.py + docs/crt/{coq_demo.v,isabelle_demo.thy}; report-only, trust boundary unchanged.
References
- The Rocq Development Team. (2025). The Rocq Prover (Version 9.0) [Computer software]. Inria, CNRS, and contributors. https://rocq-prover.org/
- Nipkow, T., Paulson, L. C., & Wenzel, M. (2025). Isabelle/HOL: A proof assistant for higher-order logic (Isabelle2025) [Computer software]. Technische Universität München & University of Cambridge. https://isabelle.in.tum.de/
- de Moura, L., & Ullrich, S. (2021). The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28 (pp. 625–635). Springer. https://lean-lang.org/