Citation revision history

Revision 1 · SyncFree: Isabelle verification of state-based CRDT implementations

Original citation · jungle

https://github.com/SyncFree/isabelle_crdt_verification

src/framework; src/crdts; README specifies Isabelle 2013-2

Public mechanized framework and implementation/convergence/specification proofs for state-based CRDTs. Apache-2.0. Useful for generalizing this concrete union-fold safety lemma to full replicated-object specifications. Inspected repository documentation and source organization; not rebuilt with its historical toolchain. This external Isabelle development is distinct from the Lean checker result on this page.

Revision 2 · SyncFree: Isabelle verification of state-based CRDT implementations

Record structured proof provenance from the earlier source harvest. Inspection depth and outstanding pinning/reproduction work remain explicit; external evidence does not change exact Hunchroom verification. · jungle

https://github.com/SyncFree/isabelle_crdt_verification

src/framework; src/crdts; README specifies Isabelle 2013-2

Public mechanized framework and implementation/convergence/specification proofs for state-based CRDTs. Apache-2.0. Useful for generalizing this concrete union-fold safety lemma to full replicated-object specifications. Inspected repository documentation and source organization; not rebuilt with its historical toolchain. This external Isabelle development is distinct from the Lean checker result on this page.

External evidence (contributor report)

mechanization reported

Proof assistant / theorem

Isabelle ·

Commit / toolchain / license

· README specifies Isabelle 2013-2; not reproduced here · Apache-2.0

Assumptions

Repository framework and CRDT-specific specifications; exact theorem and commit still need pinning.