22 Machine-Checked Theorems
Runtime-gated. Ed25519-signed. Lean 4-verified.
AgentHALO doesn't just claim security — it proves it. 22 theorems from HeytingLean (a 760K-line Lean 4 verification framework) are bound to runtime operations through a formal proof gate. Each theorem is cryptographically signed and linked to a specific Lean declaration. 74 local Lean mirror modules provide self-contained verification.
Interactive Proof Lattice
Proof Gate Configuration
14 theorem requirements across 6 tool surfaces. Each requirement binds: exact canonical FQN, declaration-line SHA-256, Heyting commit hash, and Ed25519 signature.
execute_sql3 requirementscontainer_launch2 requirementscommit3 requirementsevm_sign2 requirementskem_encapsulate1 requirementstrace_analysis3 requirementsAdvisory mode (enabled: false). The gate evaluates certificates but does not block operations. Dashboard and API simulate results and label them as advisory. Enforcement activates when certificate generation is part of operator workflow.
Rust Provenance Surfaces
Five Rust modules export formal_provenance() with 22 unique canonical theorem FQNs and 19 local mirror paths.
| Module | Entries | Covers |
|---|---|---|
| security.rs | 7 | Certificate refinement, authorization, dual auth |
| ct6962.rs | 4 | RFC 6962 consistency, inclusion, append-only |
| ipa.rs | 5 | Pedersen/IPA commitment correctness, soundness, hiding |
| coherence.rs | 4 | Sheaf coherence, trace topology, component counting |
| protocol.rs | 2 | Core nucleus steps, commit certificate verification |
Mathematical Foundations
Non-Bypassable Step Dependencies
Typed proof steps (IsWitnessStep/IsChainRoot) where each step embeds its predecessor. Audit trails that are non-bypassable at the type level. 43-line kernel generates pipelines across fundamentally unrelated domains.
Trace Topology Verification
Trace topology verified through section compatibility. Connectivity preservation, component lifting, and component monotonicity are machine-checked. Ensures trace structures are globally consistent.
Fixed-Point Commitment Algebra
Commitment verification as fixed-point algebra. The same nucleus that generates Heyting logic generates cryptographic guarantees. Consistency and inclusion proofs as algebraic operations.
74 Local Lean 4 Mirror Modules
Self-contained modules under lean/NucleusDB/. They do not import Heyting modules directly. Dual provenance links canonical Heyting theorems to local mirrors.
Core/Base types and axioms
Crypto/Hash, KEM, signatures
Commitment/IPA, KZG proofs
Genesis/Seed ceremony formalization
Identity/DID, ledger properties
TrustLayer/Nucleus operator, Heyting algebra
Comms/DIDComm, hybrid KEM
Security/Parameter sets
Sheaf/Coherence conditions
Transparency/CT log properties
Contracts/EVM verification
Adversarial/Security games
Bridge/Rust-Lean bindings
Integration/End-to-end properties
Certificate Format
.lean4export signed provenance attestations binding theorem claims to a specific Heyting commit and declaration line hash.
#THMFully qualified theorem name#META commit_hashHeyting repo commit#META theorem_statement_sha256Declaration line hash#META generated_atGeneration timestamp#META signing_didSigner DID identity#META signing_key_multibaseEd25519 public key#META signature_ed25519Ed25519 signature over payloadvalidate./scripts/validate_formal_provenance.sh
generate./scripts/generate_proof_certificates.sh
verifynucleusdb verify-certificate <file>
Verifier Pipeline
Proven, Not Promised
Advisory today. Enforced when you're ready.
The proof gate evaluates certificate compliance in advisory mode. When your workflow includes certificate generation, flip the enforcement switch and every tool call requires a valid proof.