Choosing Safe and Efficient Settings for Blockchain Consensus Protocols Using Formal Verification

Hybrid finality-gadget consensus protocols expose many tunable parameters, that are usually fixed by convention. We present a three-stage verify-then-optimize method. Stage 1, a machine-checked consistency check of the quorum-intersection bound, covers 325 committee and quorum settings by counter abstraction, cross-validated by three independent models; the verdicts reduce to the two-thirds quorum rule, fix the quorum at 2f + 1, and show that the gadget stops finalizing at 75% participation. Stage 2 certifies that confirmed but unfinalized blocks resist reorganization. For a latest-message fork choice with proposer boost under random network delays, attacked by an adversary that splits its votes and times their release per validator, we compute exactly, as a Markov decision process, the worst-case probability that a block is confirmed and then reorganized within 256 slots of its proposal, and check it against an identity-level model. With 13 and 25 validators and an adversary at the gadget’s fault bound, the balancing attack succeeds almost surely unless the boost lies in a narrow window, and a risk of 10−6 requires 38 to 90 slots of confirmation, 1.5 to 3.5 times the depth a proof-of-work estimate prescribes. Stage 3 reports operating points: against such an adversary every slot length trades confirmation latency against message load.