Mirrors/yjs
1
0
Fork 0
mirror of https://github.com/yjs/yjs.git synced 2025-12-16 11:47:46 +01:00
Code Issues Packages Projects Releases Wiki Activity

add reference to lean-yjs

Browse Source
This commit is contained in:
Kevin Jahns
2025-09-15 18:35:33 +02:00
parent 5c861336ad
commit 2f47a98380
1 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
README.md
View File

@@ -1385,6 +1385,15 @@ But we use state vectors only to describe the state of the local document, so we
can compute the missing struct of the remote client. We do not use it to track
causality.
### Formal Proof
[lean-yjs](https://github.com/iasakura/lean-yjs) provides a formal verification
of the YATA CRDT algorithm that Yjs implements, using the Lean theorem prover to
mathematically prove correctness properties. While the CRDT algorithm itself is
correct (currently proven for preservation and commutativity), the project
reveals that [the pseudocode in the original YATA paper contains
errors](https://discuss.yjs.dev/t/lean-yjs-formally-proving-the-yjs-conflict-resolution-algorithms/3875/2).
## License and Author
Yjs and all related projects are [**MIT licensed**](./LICENSE).