Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Lean Ethereum PQ Crypto • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can Ethereum survive the quantum transition with formally verified cryptographic primitives? This project formalizes the post-quantum migration path: replacing ECDSA with XMSS hash-based signatures, replacing KZG polynomial commitments with Sumcheck polynomial IOPs under the Fiat-Shamir transform, and constructing PQ HTLCs for quantum-safe atomic swaps. Based on Drake and Khovratovich’s Ethereum Foundation research.
Original Researchers
Key Verified Results
xmss_verify_soundXMSS signature verification is sound
XMSS.lean
sumcheck_soundnessSumcheck protocol has negligible soundness error
Sumcheck.lean
fiat_shamir_secureFiat-Shamir transform preserves soundness in ROM
FiatShamir.lean
pq_htlc_correctPQ HTLC satisfies correctness and atomicity
PQHTLC.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 EngineerPost-Quantum Ethereum: Signature and IOP Migration
Contributor
Justin Drake
Ethereum Foundation
Core insight: Ethereum's current cryptographic stack (ECDSA, KZG) is vulnerable to quantum adversaries. Migration to hash-based signatures (XMSS) and polynomial IOPs (Sumcheck + Fiat-Shamir) provides quantum resistance while maintaining EVM compatibility through PQ HTLCs.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerPolynomial IOPs and Hash-Based Commitment Schemes
Contributor
Dmytro Khovratovich
Ethereum Foundation
Complete framework: (1) XMSS/LeanSig tree-based one-time signatures with Winternitz compression, (2) Sumcheck protocol for multivariate polynomial evaluation proofs, (3) Fiat-Shamir transform for non-interactive verification, (4) PQ HTLCs replacing ECDSA-locked hash time-locked contracts.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — PQ Ethereum Primitives
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of post-quantum cryptographic primitives for Ethereum. XMSS signature verification, Sumcheck protocol soundness, Fiat-Shamir security reduction, and PQ HTLC correctness. All proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerLean Ethereum PQ 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 + Drake/Khovratovich Reference Documentation
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with comprehensive documentation linking formalized properties to Drake and Khovratovich eprints on Ethereum post-quantum migration.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026