Resumen

Conflict-Free Replicated Data Types (CRDTs) enable distributed systems to achieve eventual consistency without coordination, making them necessary for applications such as collaborative editors, distributed databases and decentralized systems. Designing CRDTs is complex: subtle choices in merge semantics can lead to unintended divergence, and proving correctness properties such as convergence, commutativity, and idempotence requires rigorous reasoning. While existing work demonstrates that individual CRDTs can be verified using theorem provers, each verification effort typically starts from scratch, requiring substantial proof overhead for common properties. Our proposal offers a structured approach for CRDT verification by developing a modular framework in the Athena proof assistant. The framework facilitates the specification of both the syntax and operational semantics of CRDTs and guides the proof of key properties such as con- vergence, commutativity, and idempotence. By identifying and encapsulating common patterns in CRDT design and verification. It is suited to developers who are exploring or prototyping new CRDT variants and need a precise and checkable way to reason about their correctness. While the framework does not cover all possible CRDT designs. It takes a modest step toward making formal verification more approachable in this domain.