{"repo":"AU-COBRA/ConCert","free":true,"listed":false,"github":"https://github.com/AU-COBRA/ConCert","clone":"git clone https://github.com/AU-COBRA/ConCert.git","description":"A framework for smart contract verification in Coq","language":"Rocq Prover","stars":128,"topics":["blockchain","coq","smart-contracts","verification"],"license":"MIT","category":"blockchain-web3","readme_excerpt":"ConCert A framework for smart contract verification in Rocq. See the Papers for details on the development. ConCert can find real-world attacks as explained here, here, and here. How to build Our development works with Rocq 9.0 and depends on MetaRocq, and std++. The tests depend on QuickChick. The dependencies can be installed through opam . Branches compatible with older versions of Rocq/Coq can be found here. Install dependencies and build ConCert locally Installing the necessary dependencies requires the opam package manager and a switch with Rocq 9.0 installed. If you don't already have a switch set up run the following commands To install the dependencies run 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 . Example smart contracts can be built by running make examples . Install ConCert and dependencies To install ConCert in your switch run Examples can be installed by running Structure of the project Each folder contains a separate README file with more details. The embedding folder contains the development of the verified embedding of λsmart to Rocq. The execution folder contains the formalization of the smart contract execution layer, which allows reasoning about interacting contracts, and perform property-based testing. The test folder contains the property-based testing framework. The key generators used for automatically generati","default_branch":null,"files":null,"tree":[],"storefront":"/r/AU-COBRA","claimed":false,"request_supported":{"post":"https://gitbuyer.com/r/AU-COBRA/ConCert/request-supported","requests":0},"note":"indexed from public GitHub; nothing is for sale on this page. Clone it from GitHub. Paid listings live at /search."}