Formalizing Accountable Liveness for Provable Consensus Security and Validator Punishment
Introducing Accountable Liveness and the $x$-partially-synchronous model to formally identify and punish consensus-stalling nodes, strengthening BFT security.
