Design and Verification of Byzantine Fault Tolerant CRDTs

Decentralized collaboration systems offer powerful solutions for various applications. For instance, Wikipedia currently requires significant operational costs to maintain its servers, but a decentralized alternative could run without such constraints. However, maintaining data consistency across peers remains challenging in such decentralized systems. While Conflict-free Replicated Data Types (СRDTs) can maintain consistency without central server, they lack resilience against Byzantine faults. This project introduces a framework for designing and verifying Byzantine Fault Tolerant (BFT) CRDTs in Isabelle/HOL. It requires modest modifications to existing CRDTs, and relies on minimal assumptions on the system.