ConCert

Contract Verifier

A framework for verifying smart contracts in Coq, a proof assistant language.

A framework for smart contract verification in Coq

GitHub

0 stars
0 watching
0 forks
Language: Coq
last commit: about 2 years ago

Related projects:

Repository Description Stars
frederikvigen/concert A framework for verifying smart contracts in Coq to ensure their correctness and security 0
siimplex/concert A framework for verifying smart contracts in Coq 1
au-cobra/concert A framework for verifying smart contracts in Coq using formal methods and property-based testing. 114
astenbaek/atpl-project A framework for verifying smart contracts using Coq 0
certigraph/certigraph A verification toolset for graph-manipulating programs written in Coq. 17
coq-community/chapar A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant 32
tezos/tezoscoq A Coq-based library providing a formal verification framework for the Tezos smart contract language 28
sri-csl/solidity An automated verifier for the Solidity programming language used in smart contracts on the Ethereum platform. 50
jscert/jscert A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter 196
ethereum/sourcify A decentralized service for verifying the integrity of smart contract source code on Ethereum. 786
sec-bit/tokenlibs-with-proofs Verifies the correctness of Ethereum token contracts using formal methods and proof assistants. 98
formal-land/coq-of-python Formal verification of Python code using Coq 30
verifid/graph-vl An identity verification system with GraphQL and Postgres database 59
runtimeverification/avm-semantics A tool for formally verifying Algorand smart contracts' behavior using property-based testing and symbolic execution 15
veridise/medjai A symbolic execution tool for verifying the correctness of smart contracts written in Cairo. 49