ssprove
Cryptographic proof framework
A foundational framework for formalizing cryptographic proofs in Coq.
A foundational framework for modular cryptographic proofs in Coq
56 stars
8 watching
10 forks
Language: Coq
last commit: 20 days ago
Linked from 2 awesome lists
coq-formalizationcoq-librarycryptographyformal-verificationmodular-cryptographic-proofsstate-separating-proofs
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 adampetcher/fcf | A framework for machine-checked proofs of cryptography in the computational model. | 48 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 distributedcomponents/disel | A framework for implementing and verifying distributed systems using Coq | 95 |
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |
 cossacklabs/themis | A cryptographic framework providing unified APIs for secure data protection across multiple platforms | 1,875 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 easycrypt/certicrypt | A framework for formal verification and validation of cryptographic proofs using Coq | 33 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 dunnl/tealeaves | A framework for abstract syntactical reasoning in Coq. | 23 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 tezos/tezoscoq | A Coq-based library providing a formal verification framework for the Tezos smart contract language | 28 |
| xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 69 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |