Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Speaking to Silicon • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
How much does your hardware leak? Every computation leaves physical traces — execution time varies with secret data, power consumption correlates with register values, electromagnetic fields radiate internal state. This project formalizes information-theoretic side-channel security in Lean 4: leakage is mutual information I(Secret; Observable) over finite probability spaces. A device is secure when this quantity is bounded. The data processing inequality proves that post-processing observables cannot increase leakage, and composition theorems handle multiple observations.
Side-Channel Leakage Model
| Channel | Physical Observable | Leakage Measure |
|---|---|---|
| Timing | Execution duration | I(key; cycles) |
| Power | Current draw | I(key; trace) |
| EM | Electromagnetic field | I(key; spectrum) |
Key Verified Results
mutual_info_nonnegMutual information is non-negative
Entropy.lean
data_processing_ineqPost-processing cannot increase leakage
Leakage.lean
composition_boundMulti-observation leakage bounded by sum
Composition.lean
constant_time_zero_leakConstant-time execution implies zero timing leakage
Leakage.lean
“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 EngineerInformation Leakage as Mutual Information
Contributor
Apoth3osis Labs
R&D Division
Core insight: silicon side-channel leakage — timing, power consumption, electromagnetic emanation — can be formalized as mutual information between secret state and observable physical quantities. A device is secure if and only if this mutual information is bounded.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerFinite Probability Theory for Side-Channel Analysis
Contributor
Apoth3osis Labs
R&D Division
Complete framework: (1) finite probability spaces over secret/observable pairs, (2) conditional entropy and mutual information definitions, (3) data processing inequality — post-processing cannot increase leakage, (4) composition theorems for multi-observation settings, (5) bounds on min-entropy leakage for worst-case adversaries.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — Information-Theoretic Side-Channel Security
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of information-theoretic side-channel security. Finite probability spaces, mutual information bounds, data processing inequality, and composition theorems for multi-observation leakage. All proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerSpeaking to Silicon 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 + Side-Channel Case Studies
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with case studies applying the formal leakage model to timing, power, and EM side channels.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026