Formal Proofs
23 proofs · 111 theorems
Formal verification of consensus protocols, DeFi invariants, and cryptographic primitives using Lean 4, Halmos, and Foundry.
Formal proof of Byzantine fault tolerance safety properties including quorum intersection, honest majority guarantees, and unique decision thresholds.
The central safety theorem proving that no two honest nodes can finalize conflicting decisions under the assumed fault model.
Formal proof that the consensus protocol eventually makes progress under partial synchrony assumptions with bounded message delays.
Three theorems proving decided_stable (finalized decisions never revert), confidence_monotone (confidence only increases), and finalization (termination guarantee).
Three theorems proving cert_skip_exclusive (no conflicting certificates), honest_support (honest nodes back valid certs), and classify_total (complete classification).
Three theorems proving height_monotone (finalized height only increases), bls_quorum (BLS signature quorum validity), and dual_sig (dual-certificate consistency).
Formal verification of the Ray consensus protocol with two key theorems covering protocol safety and progress guarantees.
Two theorems verifying the Field consensus protocol properties including consistency and termination.
Two theorems verifying the Nova consensus protocol covering fast-path finality and fallback safety.
Two theorems verifying the Nebula consensus protocol properties for probabilistic finality and convergence.
Two theorems verifying the Photon consensus protocol for low-latency finality and message complexity bounds.
Two theorems verifying the Prism consensus protocol properties for parallel block processing and ordering guarantees.
Three axioms for BLS signature verification with bilinearity proved. Establishes the cryptographic foundation for aggregate signatures used in Quasar consensus.
Two axioms with real postconditions for FROST threshold signature verification, establishing correctness of t-of-n Schnorr threshold signing.
Two axioms for Ringtail post-quantum threshold signatures based on lattice cryptography, ensuring quantum resistance for consensus finality.
Two axioms for ML-DSA (FIPS 204) post-quantum digital signatures establishing correctness and unforgeability under lattice hardness assumptions.
Three proved theorems plus nonces_monotone for Warp cross-chain messaging, ensuring exactly-once delivery and replay protection.
Two proved theorems for Warp message ordering guarantees, ensuring causal consistency across chains.
Twelve symbolic proofs verifying AMM V2 invariants including constant product preservation, no-drain guarantees, output bounds, and fee correctness using Halmos symbolic execution.
Nine symbolic proofs for the LiquidLUX vault covering share inflation protection, exchange rate monotonicity, deposit/withdraw symmetry, and fee accounting correctness.
Eight symbolic proofs for the Morpho-style lending markets covering utilization bounds, interest rate monotonicity, collateral sufficiency, and liquidation safety.
Comprehensive property-based fuzzing across 33 test suites covering AMM, LiquidLUX, Markets, Perps, StableSwap, Staking, Karma, Bridge, Governance, and Treasury protocols.