Multi-prover formal verification of Certified Null Operations (CNO: programs provably computing nothing) and Observational Null Disclosure (OND: programs provably revealing nothing). Two co-equal, logically independent pillars verified across Coq, Lean 4, and Agda, with axiom counts and out-of-scope residue lists honestly surfaced.
open-source coq theorem-proving agda formal-verification proof-engineering lean4 rocq-prover reversible-computing hyperpolymath epistemic-infrastructure epistemic-computing veridical-computing equivalence-aware-computing typed-provenance certified-null-operations observational-null-disclosure multi-prover-verification
-
Updated
Oct 1, 2026 - Rocq Prover