A critical paper underlying Casper’s consensus protocol, codename Zug, is Weakly-terminating Binary Aggreement and Reliable Broadcast to Atomic Broadcast by Andreas Fackler, Samuel Schlesinger, and Matthew Doty. Here, we are drafting a formalization to machine check the pen-and-paper proofs therein.