The "correctness" section is very cool: Double-spending. Suppose some execution of the protocol produced two confirmed transactions t1 and t2 that spend the

The "correctness" section is very cool: Double-spending. Suppose some execution of the protocol produced two confirmed transactions t1 and t2 that spend the same output. Each confirmed transaction is signed by a validator quorum. Since the adversary controls at most f validators, at least f +1 correct validators signed t1 and t2. Since there are 2f +1 correct validators, some correct validator v signed both t1 and t2. However, when signing a transaction, correct validators check whether they have not signed any of the inputs previously – a contradiction.