safemesh

SafeMesh is an open-source library designed for lean, embeddable state synchronization using Conflict-free Replicated Data Types (CRDTs). Its primary distinction is the use of formal verification: the core convergence properties of five CRDT types (G-Set, G-Counter, PN-Counter, OR-Set, and RGA/Text) are backed by machine-checked proofs in Lean 4. This ensures mathematical guarantees for data consistency across distributed replicas. The library is implemented in `no_std` Rust, making it suitable for resource-constrained environments and embedded systems. SafeMesh provides a core Rust API along with bindings for C (via FFI), WASM/TypeScript, and Python. These bindings allow developers to integrate verified CRDT logic into web applications, native software, and scripting environments without reimplementing the merge logic. Key features include: - **Formal Verification**: The delta-CRDT suite is proven in Lean 4, with zero `sorry` axioms, ensuring high reliability for state-based convergence. - **Multi-Language Support**: Exposes the same Rust core through C ABI, WASM, and Python interfaces, with canonical byte encoding for wire transfer. - **Transport Agnostic**: SafeMesh handles the CRDT state and event log plumbing (append/merge/since), but users must provide their own transport mechanism for network communication. - **Testing Infrastructure**: Includes differential testing against Lean-generated oracle corpora, laws harnesses for custom types, and CI gates to maintain proof integrity. The project explicitly scopes its guarantees, distinguishing between proven CRDTs and other tested-but-not-proven types like LWW Register and LWW Map. It is licensed under Apache-2.0.