Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Hybrid Crypto QKD + PQ-KEM • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can we build a key establishment protocol that survives both quantum and classical attacks? Neither QKD alone (vulnerable to implementation side-channels) nor post-quantum KEMs alone (relying on unproven hardness assumptions) provide unconditional security. This project formalizes a UC composable hybrid combining both: security holds as long as at least one component remains unbroken — the “either breaks” property. References the X-Wing hybrid KEM and aligns with NIST FIPS 203.
Key Verified Results
either_breaksSecurity holds if QKD OR PQ-KEM is unbroken
EitherBreaks.lean
uc_realizes_idealHybrid protocol UC-realizes ideal key establishment
UCFramework.lean
simulator_soundnessSimulator indistinguishable from real execution
UCFramework.lean
composition_secureHybrid composes securely with arbitrary protocols
Composition.lean
Hybrid Protocol Architecture
| Component | Threat Model | Role in Hybrid |
|---|---|---|
| QKD | Information-theoretic | Unconditional key if channel is authentic |
| PQ-KEM | Computational (lattice) | Backup key if QKD channel compromised |
| Hybrid | Either-breaks | XOR of both keys: secure if either holds |
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is cryptographically anchored with IPFS CIDs.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerHybrid Key Establishment: QKD + PQ-KEM
Contributor
Apoth3osis Labs
R&D Division
Core insight: neither quantum key distribution nor post-quantum KEMs alone provide unconditional security against both quantum and classical adversaries. A UC composable hybrid protocol combining both achieves the 'either breaks' property — security holds as long as at least one component remains unbroken.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerUC Framework for Hybrid Key Establishment
Contributor
Apoth3osis Labs
R&D Division
Complete UC composability framework: ideal functionality for hybrid key establishment, simulator construction, environment indistinguishability proof. The either-breaks property is captured formally: if QKD is secure OR if PQ-KEM is secure, then the hybrid protocol realizes the ideal functionality.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — UC Composable Hybrid Key Establishment
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the UC hybrid key establishment protocol. Proves either-breaks property, simulator soundness, and composition with arbitrary protocols. All proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerHybrid Crypto Verified Kernel
Contributor
Apoth3osis Labs
R&D Division
All theorems kernel-checked by Lean 4. Guard-no-sorry passes. Standard axioms only.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerStandalone Repository + NIST Alignment Documentation
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with comprehensive documentation linking formalized properties to NIST FIPS 203 requirements and X-Wing hybrid KEM specification.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026