disel
Distributed system framework
A framework for implementing and verifying distributed systems using Coq
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
95 stars
13 watching
7 forks
Language: Coq
last commit: 7 months ago coqcoq-librarydistributed-systemsmathcompproofseparation-logicssreflecttwo-phase-commit
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 595 |
 cmeiklejohn/distributed-data-structures | An implementation of various distributed data structures in Coq, including lattices and Convergent Replicated Data Types. | 49 |
| uwplse/verdi-raft | An implementation of the Raft distributed consensus protocol verified in Coq | 186 |
 ssprove/ssprove | A foundational framework for modular cryptographic proofs in Coq | 56 |
 logsem/aneris | A framework for developing and verifying distributed systems using separation logic | 33 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
| coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 70 |
| imdea-software/fcsl-pcm | A formalisation of Partial Commutative Monoids (PCMs) for verification of concurrent programs. | 26 |
 dunnl/tealeaves | A framework for abstract syntactical reasoning in Coq. | 23 |
 south-hw/fedpara_iclr22 | A collaborative deep learning framework that enables private and efficient model updates in distributed settings | 9 |
 verse-lab/toychain | A minimalistic blockchain-based consensus protocol implemented in Coq | 111 |
 heades/system-f-coq | An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
 jepst/cloudhaskell | A distributed computing framework for building fault-tolerant and redundant applications | 347 |