A Framework for Designing and Verifying Byzantine Fault Tolerant CRDTs To check the proof, run isabelle build -D . in the root directory of this repository.