tezoscoq
Contract verification framework
A Coq-based library providing a formal verification framework for the Tezos smart contract language
working with coq and tezos
28 stars
13 watching
9 forks
Language: Coq
last commit: about 9 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
 astenbaek/atpl-project | A framework for verifying smart contracts using Coq | 0 |
 josefgit/concert | A framework for verifying smart contracts in Coq, a proof assistant language. | 0 |
 siimplex/concert | A framework for verifying smart contracts in Coq | 1 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 au-cobra/concert | A framework for verifying smart contracts in Coq using formal methods and property-based testing. | 114 |
 sec-bit/tokenlibs-with-proofs | Verifies the correctness of Ethereum token contracts using formal methods and proof assistants. | 97 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 157 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| 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 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 frederikvigen/concert | A framework for verifying smart contracts in Coq to ensure their correctness and security | 0 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |