safemesh

SafeMesh は、衝突回避型レプリカデータ型（CRDT）を使用した、軽量で組み込み可能な状態同期のためのオープンソースライブラリです。その特徴は、形式検証の活用にあり、5 つの 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 で生成されたオラクルコーパスに対する差分テスト、カスタムタイプ用の法則ハーネス、および証明の整合性を維持するための CI ゲートが含まれています。 このプロジェクトは、保証の範囲を明確に定義しており、検証済みの CRDT と、LWW Register や LWW Map などのテスト済みだが検証されていないタイプを区別しています。ライセンスは Apache-2.0 です。