CITATION.cff

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
type: software
title: "Absolute Zero"
abstract: "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 mechanised in several provers, including Coq, Lean 4 and Agda, with axiom counts and out-of-scope residue lists honestly surfaced."
authors:
  - family-names: "Jewell"
    given-names: "Jonathan D.A."
    orcid: "https://orcid.org/0000-0002-3078-6652"
repository-code: "https://github.com/hyperpolymath/absolute-zero"
keywords:
  - "coq"
  - "agda"
  - "lean4"
  - "formal-verification"
  - "epistemic-computing"
  - "epistemic-infrastructure"
  - "equivalence-aware-computing"
  - "hyperpolymath"
  - "open-source"
  - "rocq-prover"
  - "theorem-proving"
  - "typed-provenance"
  - "veridical-computing"
  - "certified-null-operations"
  - "multi-prover-verification"
  - "observational-null-disclosure"
  - "proof-engineering"
  - "reversible-computing"