AVantGaRDe

The *AVantGaRDe* (Verified highly-Available and Reliable Distributed Graph Databases) project aims to develop a framework for reliably supporting local-first connectivity. Graph databases have recently been introduced to efficiently manage interconnected, heterogeneous, and semi-structured data. These leverage native graph storage, an expressive property graph model, and dedicated graph query languages. Still, scalably and reliably managing large graphs, while ensuring availability, low latency, and consistency is challenging. While cloud graph databases try to address this, local-first solutions allow users to preserve ownership and agency over their data. Unfortunately, no local-first graph databases exist, as these require customized replicated data types (CRDTs) and compositionally preserving graph invariants. Moreover, as CRDTs are already notoriously difficult to construct, ensuring the correctness of complex graph CRDTs is challenging. The project aims to develop a novel framework for designing foundational models for local-first graph databases, with built-in trustworthiness and reliability guarantees. *AVantGaRDe* sets to design a unified framework for prototyping and extracting correct-by-construction horizontally scaled property graph CRDTs that can preserve complex invariants.