Why is Erasure Before WAL important?

Standard write-ahead logging (WAL) records a transaction before executing it. For key destruction, this means a crash during finalization could resurrect the compromised classical keys from the WAL journal. The Higgaion engine inverts this sequence: key material is erased with OPENSSL_cleanse() before the WAL commit, ensuring deterministic crash recovery.

What is the Store Now, Decrypt Later threat?

Store Now, Decrypt Later (SNDL) is an attack strategy where adversaries harvest encrypted data and public keys today, intending to decrypt them once quantum computers can break classical algorithms. This makes migration urgent even before quantum computers are available.

Knowledge Base

Frequently Asked Questions

Q: What formal verification does the Higgaion engine use?

The engine uses quad-tier formal verification: TLA+ model checking for liveness and safety properties, CBMC bounded model checking for pointer safety and undefined behavior, Frama-C WP deductive verification for function contracts, and Coq mechanized proofs for state machine invariants. Over 101 Coq theorems compile with zero admitted lemmas.

Post-Quantum Cryptography

What is post-quantum cryptography?

Post-quantum cryptography (PQC) refers to cryptographic algorithms that are resistant to attacks by both classical and quantum computers. In August 2024, NIST finalized the first PQC standards after an 8 year evaluation: ML-KEM (FIPS 203) for key encapsulation and ML-DSA (FIPS 204) for digital signatures. These lattice-based algorithms provide long-term security against Shor's algorithm, which would break all currently deployed ECDSA, RSA, and Ed25519 cryptography.

What is ML-DSA-87?

ML-DSA-87 (Module-Lattice Digital Signature Algorithm, security level 5) is the highest security parameter set defined by FIPS 204. It provides 256 bit equivalent security against both classical and quantum attacks. The Higgaion PQC Migration Engine uses ML-DSA-87 for all post-quantum digital signatures, generating dual classical/PQC signatures during the HYBRID migration state.

What is ML-KEM-1024?

ML-KEM-1024 (Module-Lattice Key Encapsulation Mechanism, security level 5) is defined by FIPS 203. It replaces RSA and ECDH for key exchange and transport. The Higgaion engine generates ML-KEM-1024 keypairs during migration self-tests to validate that the PQC implementation is functioning correctly before committing a key to the HYBRID state.

What is CNSA 2.0?

CNSA 2.0 (Commercial National Security Algorithm Suite 2.0) is the NSA's mandate for migrating all national security systems to post-quantum cryptography. It requires software and firmware implementations to adopt ML-KEM-1024 and ML-DSA-87 by 2030, with hardware and ASIC implementations following by 2033. CNSA 2.0 compliance is mandatory for all U.S. defense contractors and national security systems.

The Migration Engine

What is disjunctive hybrid verification?

Disjunctive (OR-mode) hybrid verification accepts a message as valid if either the classical or the post-quantum signature verifies independently. This is the opposite of conjunctive (AND-mode) approaches like IETF composite signatures, which require both to pass. Disjunctive verification enables zero-downtime migration across networks where not all nodes have upgraded simultaneously. Legacy nodes continue to verify classical signatures while upgraded nodes verify PQC signatures.

What is Erasure Before WAL?

Write-ahead logging (WAL) normally records a transaction before executing it, so crashes can be recovered by replaying the log. For cryptographic key destruction, this is fatally flawed: if the system crashes after the WAL records "finalize" but before the key is actually erased, recovery replays the log and the compromised key material survives. The Higgaion engine inverts this sequence. Classical key material is irrecoverably wiped using OPENSSL_cleanse() before the WAL records the transition. If a crash occurs after erasure but before the WAL write, the key remains in the HYBRID state (safe), but the classical material is already gone (secure). Patent pending.

What migration states does a key go through?

Each key transitions through four states: CLASSICAL (only the original ECC key exists), HYBRID (both classical and ML-DSA-87 keypairs are active, dual signatures are produced), FINALIZING (PQC self-test passed, awaiting administrator confirmation), and PQC_ONLY (classical key material irreversibly erased). The transition from FINALIZING to PQC_ONLY is strictly irreversible. Rollback is permitted from HYBRID and FINALIZING back to CLASSICAL.

What key formats does the engine support?

The multi-chain import system supports Bitcoin (WIF with Base58Check), Ethereum (hex with Keccak-256 address derivation and EIP-55 checksums), ECDSA (DER-encoded P-256 and P-384 curves), and Ed25519 (32 byte seeds with Solana, Cardano, and generic address derivation). All imported keys receive a universal SHA3-256 identifier that remains stable across the entire migration lifecycle.

Verification and Security

What formal verification does the Higgaion engine use?

The engine employs quad-tier formal verification: (1) TLA+ model checking across 3 specifications with 16 safety invariants; (2) CBMC bounded model checking for pointer safety, buffer bounds, and undefined behavior; (3) Frama-C WP deductive verification with 40 ACSL annotations for function-level contracts; and (4) Coq (Rocq) mechanized proofs with over 101 theorems that compile with absolutely zero admitted lemmas.

What does "zero admitted lemmas" mean?

In Coq, an Admitted command allows a theorem to be assumed true without proof. It is commonly used as a placeholder during development. Zero admitted lemmas means every single theorem in the Higgaion Coq development has been fully proved from first principles. There are no assumed axioms, no skipped proofs, and no placeholders. The Coq compiler independently verifies every proof.

What is the pre-migration self-test?

Before any key transitions from CLASSICAL to HYBRID, the engine performs a cryptographic self-test: it generates an ML-DSA-87 keypair and ML-KEM-1024 keypair, signs a predetermined test message with a domain separation tag, and verifies the signature. If verification fails, both PQC keypairs are destroyed and the transition is aborted. This prevents migration to a faulty PQC implementation.

Deployment

What dependencies does the engine require?

The PQC Migration Engine is a standalone C library with no dependencies beyond OpenSSL 3.5+, which provides native ML-DSA-87 and ML-KEM-1024 support. It builds with GCC or Clang on Linux. No third-party PQC providers, external frameworks, or runtime dependencies are required.

Is the engine open source?

The core cryptographic primitives, formal verification artifacts (TLA+ specifications, Coq proofs, CBMC harnesses), and the Enterprise Gateway are open source on GitHub. The full PQC Migration Engine is available for commercial licensing. Contact us for enterprise deployment options.

Is there a patent on the technology?

A provisional patent application covering the crash-recoverable PQC migration state machine, the Erasure Before WAL technique, and disjunctive hybrid verification was filed with the USPTO on March 9, 2026. A full non-provisional patent application is in preparation.

Ethics & Transparency

Is this project built using AI assistance?

Yes. In the spirit of radical transparency, we explicitly disclose that the Higgaion Protocol is engineered alongside advanced AI pair-programming agents. We believe acknowledging AI-assisted development is an ethical imperative in modern cryptography to combat the illusion of singular "independent" genius. However, AI does not replace rigor: the machine writes the code, but mathematics verifies it. Every mechanism is subjected to our quad-tier formal verification pipeline (TLA+, CBMC, Frama-C, and Coq). We do not rely on empirical testing alone; we demand mathematical proof.