Why Formal Verification Matters
In blockchain systems, a consensus bug is not a minor inconvenience — it can mean permanent loss of funds. While many protocols rely on informal arguments or simulation-based testing, COOL takes a different approach. We have subjected our adaptive consensus mechanism to formal verification using the TLA+ specification language and the Isabelle/HOL proof assistant.
The result is a mathematically proven guarantee that the protocol maintains safety (no conflicting blocks are finalized) and liveness (the chain continues to make progress) under our stated assumptions.
Key Results
The research paper establishes several important properties:
- Byzantine fault tolerance up to f < n/3 — The protocol tolerates up to one-third malicious validators without compromising safety or liveness
- Adaptive parameter safety — Dynamic adjustments to batch size, timeout intervals, and lane allocation preserve all safety invariants
- Finality latency bounds — Under normal network conditions, finality is achieved within 380ms with 95th percentile confidence
- Throughput scaling — Linear throughput scaling up to 128 lanes, with sub-linear degradation beyond that threshold
Benchmarks: COOL vs. Existing L1s
We ran standardized benchmarks across five major L1 networks and compared key metrics. The results demonstrate COOL's advantages in finality speed and adaptive throughput:
Adversarial Testing
Beyond theoretical proofs, we subjected the protocol to extensive adversarial simulations. Our test suite includes scenarios such as network partitions lasting up to 30 minutes, coordinated Byzantine attacks by 32% of the validator set, sudden validator churn (50% rotation within a single epoch), and targeted denial-of-service against the block proposer.
In all tested scenarios, the protocol maintained safety. Liveness was temporarily affected during extreme partition events but recovered within 2 seconds of network reconnection.
The Adaptive Consensus Algorithm
At the heart of COOL is a three-phase consensus mechanism. The first phase (Propose) uses a deterministic leader election with VRF-based randomness. The second phase (Vote) collects threshold signatures from the validator set. The third phase (Commit) produces a quorum certificate that represents irreversible finality.
What makes COOL unique is that the parameters governing each phase — batch sizes, timeout durations, and lane counts — adjust dynamically based on a feedback loop that monitors network utilization, latency percentiles, and validator responsiveness.
Open Access
We believe in open science. The full research paper, including all proofs, benchmark methodology, and raw data, is available for download. We welcome review from the academic community and independent researchers. Send feedback to info@cool.icu.