Русский
Formal Verification and Censorship Resistance of Byzantine Consensus Protocols: An IBFT Case Study
Ziborov K. V., Bondarev N. S., Yanovich Y. A.
Received: 21 Jan 2026 Accepted: 19 Mar 2026
Published: 2026, vol. 30, issue 1, pp. 58–86
Abstract
We present a formal study of the Istanbul BFT (IBFT) protocol family that connects its vulnerable early design, corrected intermediate variants, and a censorship-resistant modification within a unified verification framework. Using TLA+ specifications and TLC model checking, we (i) obtain counterexample traces demonstrating safety violations in the first IBFT version, (ii) verify safety and liveness for a corrected QBFT variant, and (iii) formalize censorship resistance for leader-based Byzantine consensus as a bounded chain-quality requirement and show that standard leader rotation can violate it. We then introduce and verify the f-skip leader-selection rule, which enforces censorship resistance while preserving the original safety and liveness guarantees.
Keywords: IBFT, QBFT, Byzantine consensus, formal verification, TLA+, TLC, censorship resistance.
BibTeX
@article{IS-Ziborov-Bondarev-Yanovich2026,
author = {Ziborov, Kirill Viktorovich and Bondarev, Nikita Sergeevich and Yanovich, Yury Aleksandrovich},
title = {{Formal Verification and Censorship Resistance of Byzantine Consensus Protocols: An IBFT Case Study}},
journal = {Intelligent Systems. Theory and Applications},
year = {2026},
volume = {30},
number = {1},
pages = {58--86},
}
AMSBIB
\Bibitem{IS-Ziborov-Bondarev-Yanovich2026}
\by K.\,V.~Ziborov, N.\,S.~Bondarev, Y.\,A.~Yanovich
\paper Formal Verification and Censorship Resistance of Byzantine Consensus Protocols: An IBFT Case Study
\jour Intelligent Systems. Theory and Applications
\yr 2026
\vol 30
\issue 1
\pages 58--86
\lang In Russian