safemesh

SafeMesh é uma biblioteca de código aberto projetada para sincronização de estado enxuta e incorporável usando Tipos de Dados Replicados sem Conflito (CRDTs). Sua principal distinção é o uso de verificação formal: as propriedades de convergência do núcleo de cinco tipos de CRDT (G-Set, G-Counter, PN-Counter, OR-Set e RGA/Text) são respaldadas por provas verificadas por máquina em Lean 4. Isso garante garantias matemáticas para a consistência dos dados entre réplicas distribuídas. A biblioteca é implementada em Rust no_std, tornando-a adequada para ambientes com recursos limitados e sistemas embarcados. SafeMesh fornece uma API Rust central, juntamente com bindings para C (via FFI), WASM/TypeScript e Python. Esses bindings permitem que os desenvolvedores integrem a lógica de CRDT verificada em aplicativos da web, software nativo e ambientes de script sem reimplementar a lógica de mesclagem. Recursos principais incluem: - **Verificação Formal**: A suíte delta-CRDT é provada em Lean 4, com zero axiomas 'sorry', garantindo alta confiabilidade para a convergência baseada em estado. - **Suporte a Múltiplos Idiomas**: Expõe o mesmo núcleo Rust por meio de ABI C, WASM e interfaces Python, com codificação de bytes canônica para transferência via fio. - **Agnóstico ao Transporte**: SafeMesh lida com o estado do CRDT e a canalização do log de eventos (append/merge/since), mas os usuários devem fornecer seu próprio mecanismo de transporte para comunicação de rede. - **Infraestrutura de Testes**: Inclui testes diferenciais contra corpora de oráculos gerados por Lean, harnesses de leis para tipos personalizados e gates de CI para manter a integridade das provas. O projeto delimita explicitamente suas garantias, distinguindo entre CRDTs comprovados e outros tipos testados, mas não comprovados, como LWW Register e LWW Map. É licenciado sob Apache-2.0.