Skip to content
A framework for smart contract verification in Coq
Coq JavaScript CSS Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
embedding
execution
extra
extraction/theories
vendor/record-update
.editorconfig
.gitignore
.gitlab-ci.yml
LICENSE
Makefile
README.md
_CoqProject

README.md

ConCert

A framework for smart contract verification in Coq

How to build

Our development works with Coq 8.9.1. and depends on MetaCoq 1.0~alpha+8.9 and the std++ library v.1.2.1. These dependencies can be installed through opam.

Install Coq (see https://coq.inria.fr/opam-using.html for detailed instructions on how to manage multiple Coq installations using opam).:

opam install coq.8.9.1

Then MetaCoq:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-metacoq.1.0~alpha+8.9

And std++:

opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-stdpp.1.2.1

After completing the procedures above, run make to build the development, and make html to build the documentation. The documentation will be located in the docs folder after make html.

Structure of the project

The embedding folder contains the development of the embedding. The execution folder contains the formalization of the smart contract execution layer, which allows reasoning about interacting contracts.

You can’t perform that action at this time.