इस प्रोजेक्ट के बारे में

SafeMesh — это библиотека с открытым исходным кодом, предназначенная для легкой, встраиваемой синхронизации состояния с использованием конфликтно-независимых реплицируемых типов данных (CRDT). Ее основное отличие — использование формальной верификации: основные свойства конвергенции пяти типов CRDT (G-Set, G-Counter, PN-Counter, OR-Set и RGA/Text) подкреплены машиночитаемыми доказательствами в Lean 4. Это обеспечивает математические гарантии согласованности данных между распределенными репликами. Библиотека реализована на Rust без std, что делает ее подходящей для сред с ограниченными ресурсами и встраиваемых систем. SafeMesh предоставляет основное API на Rust, а также привязки для C (через FFI), WASM/TypeScript и Python. Эти привязки позволяют разработчикам интегрировать верифицированную логику CRDT в веб-приложения, нативное ПО и скриптовые среды без необходимости переписывать логику слияния. Ключевые особенности включают: - **Формальная верификация**: Сюита delta-CRDT доказана в Lean 4, без каких-либо «sorry»-аксиом, что обеспечивает высокую надежность для конвергенции на основе состояния. - **Поддержка нескольких языков**: Раскрывает одно и то же ядро Rust через ABI для C, WASM и интерфейсы Python, с каноническим байтовым кодированием для передачи по сети. - **Независимость от транспорта**: SafeMesh обрабатывает состояние CRDT и логику журнала событий (append/merge/since), но пользователи должны предоставить собственный механизм транспорта для сетевой коммуникации. - **Инфраструктура тестирования**: Включает дифференциальное тестирование против оракулов, сгенерированных Lean, тестовые стенды для пользовательских типов и CI-гейты для поддержания целостности доказательств. Проект явно ограничивает свои гарантии, различая доказанные CRDT и другие протестированные, но не доказанные типы, такие как LWW Register и LWW Map. Он распространяется под лицензией Apache-2.0.