Kernel-checked certification of QLDPC decoder outputs: Lean 4 verified checkers, two-sided per-run certificates (success AND failure witnesses), HMAC-chained audit logs, and Lean-emitted synthesizable RTL (1–2k gates, measured). Bivariate bicycle codes, 72–288 qubits. GPLv3 / commercial dual-license.
fault-tolerance theorem-proving rtl quantum-computing verilog audit-log formal-verification mathlib quantum-error-correction superconducting lean4 qldpc bivariate-bicycle-codes bivariate-bicycle certifying-algorithms
-
Updated
Jul 6, 2026 - Lean