Crash-Recoverable Post-Quantum Key Migration with Disjunctive Hybrid Verification
Thomas W Rodriguez Jr. | Higgaion Protocol Engineering
March 2026 | Patent Pending
Abstract
The transition from classical elliptic-curve cryptography to post-quantum algorithms is an urgent infrastructure challenge, yet existing migration approaches require all-or-nothing upgrades, lack crash recovery, and mandate conjunctive verification that prevents incremental deployment. We present a PQC Wallet Migration Engine: a standalone C library implementing a four-state crash-recoverable migration state machine with write-ahead log (WAL) atomicity, disjunctive hybrid dual-signing, and multi-chain key import. The engine migrates keys through CLASSICAL, HYBRID, FINALIZING, and PQC_ONLY states, with each transition journaled for crash recovery. In HYBRID mode, dual classical/ML-DSA-87 signatures support disjunctive (accept-either) verification, enabling zero-downtime migration across networks of mixed-capability verifiers.
Key Contributions
Crash-Recoverable State Transitions
Each key's migration state is journaled to a write-ahead log with CRC32 integrity checking and monotonic sequence numbers, providing atomic state transitions that survive process crashes and power failures.
Disjunctive Hybrid Verification
Unlike IETF composite signatures which require conjunctive (AND-mode) verification, the engine accepts a message as valid if either the classical or PQC signature verifies independently, enabling zero-downtime migration.
Multi-Chain Key Import
Format-specific adapters import keys from Bitcoin (WIF), Ethereum (hex with Keccak-256), ECDSA (DER for P-256/P-384), and Ed25519 (Solana, Cardano) with a universal SHA3-256 identifier stable across the migration lifecycle.
Pre-Migration Self-Test Gating
An operation-specific ML-DSA-87 sign/verify round-trip gates each individual key transition, distinct from any module-level initialization self-test, preventing migration to a faulty PQC implementation.
Quad-Tier Formal Verification
TLA+ model checking (3 specs, 16 invariants), CBMC bounded model checking (13 harnesses), Frama-C WP deductive verification (40 ACSL annotations), and Coq mechanized proofs (101 theorems, zero admitted).
Erasure Before WAL
The engine inverts standard WAL ordering during finalization: key material is erased with OPENSSL_cleanse() before the WAL commit, preventing crash recovery from resurrecting compromised classical keys.
Implementation
The engine is implemented as a standalone C library (4,346 lines including headers) with no dependencies beyond OpenSSL 3.5+. It builds with GCC or Clang on Linux and links against libssl and libcrypto for native ML-DSA-87 and ML-KEM-1024 support.
The full test suite of 26 lifecycle tests executes in under 500ms on commodity hardware, with Address Sanitizer (ASan) and Undefined Behavior Sanitizer (UBSan) enabled. The per-test average of 24.8ms includes ML-DSA-87 key generation, signing, and verification.
No identified prior work combines: (a) a crash-recoverable migration FSM with WAL atomicity; (b) disjunctive hybrid verification; (c) multi-chain key import; and (d) operation-specific PQC self-test gating.
Transparency Disclosure
The implementation was developed with AI coding assistants under the direction of the author. All code, architectural decisions, verification strategies, and test designs were reviewed, directed, and validated by the author. The formal verification artifacts were developed alongside the implementation by the same author, not by an independent verification team.
The system has not undergone independent third-party security audit. The formal verification provides strong guarantees about specific property classes (state machine correctness, memory safety, crash recovery ordering), but does not substitute for a comprehensive adversarial security review.
Read the Full Paper
The complete whitepaper includes detailed system design, WAL record format specifications, performance benchmarks, related work analysis, and the quad-tier formal verification methodology.