safemesh

SafeMesh es una biblioteca de código abierto diseñada para la sincronización de estado ligera y embebida utilizando Tipos de Datos Replicados Libres de Conflictos (CRDTs). Su principal distinción es el uso de verificación formal: las propiedades de convergencia centrales de cinco tipos de CRDT (G-Set, G-Counter, PN-Counter, OR-Set y RGA/Text) están respaldadas por pruebas comprobadas por máquina en Lean 4. Esto garantiza garantías matemáticas para la consistencia de datos entre réplicas distribuidas. La biblioteca está implementada en Rust no_std, lo que la hace adecuada para entornos con recursos limitados y sistemas embebidos. SafeMesh proporciona una API de Rust central junto con enlaces para C (a través de FFI), WASM/TypeScript y Python. Estos enlaces permiten a los desarrolladores integrar la lógica de CRDT verificada en aplicaciones web, software nativo y entornos de scripting sin reimplementar la lógica de fusión. Características clave incluyen: - **Verificación Formal**: La suite de delta-CRDT está probada en Lean 4, con cero axiomas 'sorry', asegurando alta fiabilidad para la convergencia basada en estado. - **Soporte Multilenguaje**: Expone el mismo núcleo de Rust a través de ABI de C, WASM e interfaces de Python, con codificación de bytes canónica para la transferencia por cable. - **Agnóstico al Transporte**: SafeMesh maneja el estado del CRDT y la plomería del registro de eventos (append/merge/since), pero los usuarios deben proporcionar su propio mecanismo de transporte para la comunicación de red. - **Infraestructura de Pruebas**: Incluye pruebas diferenciales contra oráculos generados por Lean, arneses de leyes para tipos personalizados y puertas de CI para mantener la integridad de las pruebas. El proyecto delimita explícitamente sus garantías, distinguiendo entre CRDTs probados y otros tipos probados pero no probados como LWW Register y LWW Map. Está licenciado bajo Apache-2.0.