safemesh

SafeMesh 是一个开源库，用于使用冲突自由复制数据类型（CRDT）进行精简、可嵌入的状态同步。其主要特点是使用形式验证：五个 CRDT 类型（G-Set、G-Counter、PN-Counter、OR-Set 和 RGA/Text）的核心收敛属性由 Lean 4 中的机器检查证明支持。这确保了跨分布式副本的数据一致性的数学保证。 该库使用 no_std Rust 实现，使其适合资源受限的环境和嵌入式系统。SafeMesh 提供一个核心 Rust API，以及 C（通过 FFI）、WASM/TypeScript 和 Python 的绑定。这些绑定允许开发人员将经过验证的 CRDT 逻辑集成到 Web 应用程序、原生软件和脚本环境中，而无需重新实现合并逻辑。 关键特性包括： - **形式验证**：delta-CRDT 套件在 Lean 4 中经过证明，没有 sorry 公理，确保状态收敛的高可靠性。 - **多语言支持**：通过 C ABI、WASM 和 Python 接口暴露相同的 Rust 核心，并使用规范的字节编码进行线上传输。 - **传输无关**：SafeMesh 处理 CRDT 状态和事件日志管道（append/merge/since），但用户必须提供自己的传输机制进行网络通信。 - **测试基础设施**：包括针对 Lean 生成的 oracle 语料库的差异测试、自定义类型的法律测试，以及用于维护证明完整性的 CI 门控。