certicrypt
Cryptography validator
A framework for formal verification and validation of cryptographic proofs using Coq
CertiCrypt Coq Framework
33 stars
10 watching
5 forks
Language: Coq
last commit: over 8 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
 certicoq/certicoq | A compiler for a subset of the C language that can be compiled with any standard C compiler, used in formal verification and proof assistance. | 136 |
| certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 35 |
 adampetcher/fcf | A framework for machine-checked proofs of cryptography in the computational model. | 48 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 ssprove/ssprove | A foundational framework for formalizing cryptographic proofs in Coq. | 56 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
| coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 shezadkhan137/required | A library to simplify validation by providing a declarative way to define and reuse validation logic across multiple fields. | 60 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 zmap/zlint | A tool for validating and enforcing conformance to X.509 certificate standards and PKI requirements. | 360 |
 aksalj/hashlibpp | Provides a simple C++ library to compute cryptographic checksums. | 15 |
 sharplispers/ironclad | A cryptographic toolkit written in Common Lisp. | 175 |