GCounter and delta-counter source plus the CRDT proof tests inspected. The tests expect KMap put/delete commutation to be refuted and KMapFixed laws to be proved: the artifact includes failures as well as successes. These are SMT obligations and declared test expectations, not a replayed proof run or a Lean certificate of this target.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Other · CvRDTProof.is_a_CvRDT; mergeCommutative; mergeIdempotent; mergeAssociative; KMapFixed.putDelCommute
Commit / toolchain / license
06eae81c20d9efac6c18bc5c9b67584386faa893 · VeriFx 1.0.3; Scala 2.13.1; sbt 1.9.4; Z3 backend version not independently pinned · MIT
Assumptions
Merge proofs quantify over reachable states and pairwise compatible states.
Equality may be a datatype-defined observational equals method.
The SMT solver and translation are part of the trusted verification boundary.
Reproduction
cd "examples/CRDT Verification" && sbt test
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
Move.thy and Move_Acyclic.thy establish structural safety alongside convergence. Move_SEC.thy instantiates the AFP strong_eventual_consistency locale. These tree-move results are substantially richer than the posted grow-only-set target, and need their own formal targets to claim exact Hunchroom verification.
6c23447c12a7862ff31b7fc2205f6c90fbdb9dc0 · README demonstrates Isabelle2019; requires AFP CRDT and Collections sessions · MIT
Assumptions
Operations have distinct timestamps; equal delivered operation sets are compared.
SEC is instantiated in the causal-network framework with its delivery assumptions.
Reproduction
cd proof && isabelle build -D .
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
Isabelle/HOL mechanization reported in thesis; https://ttaylorr.com/publications/uw-thesis.pdf
Extends convergence reasoning to delta-state fragments and relaxed network assumptions. Relevant follow-on targets: join equivalence of delta fragments, duplication/reordering safety, and explicit eventual-delivery assumptions. Paper-reported mechanization; source/build reproduction not inspected. Does not establish network liveness from the equal-delivered-set premise used here.
External evidence (contributor report)
mechanization reported
Proof assistant / theorem
Isabelle ·
Commit / toolchain / license
· ·
Assumptions
Thesis delta-state model and network assumptions; proof source and reproduction were not inspected.
StateLib framework; artifact DOI 10.5281/zenodo.7718868; https://github.com/logsem/aneris
Mechanized distributed-program verification in Coq/Iris/Aneris: state-based CRDT implementations, modular specifications and client reasoning. A stronger implementation-level next step beyond an algebraic join-fold lemma. Public paper and repository inspected, not rebuilt; the external artifact is separate from this Lean proof and does not verify arbitrary production implementations.
External evidence (contributor report)
mechanization reported
Proof assistant / theorem
Coq ·
Commit / toolchain / license
· ·
Assumptions
Aneris/Iris distributed-program model and StateLib specifications; paper and repository overview inspected, exact theorem/toolchain still need pinning.
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.