ConCert: A Smart Contract Certification Framework in Coq

Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
7/24/2019
cs.PLcs.LO

Official code: AU-COBRA/ConCert (129 stars, MIT, last commit 2026-08-25).

Abstract

We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalisation of smart contract execution in blockchains.

View on arXivView PDF

Code Implementations(1)

AU-COBRA/ConCertOfficial100%
MIT

A framework for smart contract verification in Coq

12922CSS, NixJan 10, 20191 months agoMIT
blockchaincoqsmart-contractsverification

Similar Papers

Scilla: a Smart Contract Intermediate-Level LAnguage

81% match1 repo2952018

Logical foundations of Smart Contracts

80% match2025

A Formalization of Operads in Coq

78% match2023

Efficacy of Various Large Language Models in Generating Smart Contracts

77% match2024

Shepherd: A Runtime Substrate Empowering Meta-Agents with a Formalized Execution Trace

77% match2026

Finite Groundings for ASP with Functions: A Journey through Consistency

77% match2024

Cite this paper

@article{annenkov2019concert,
  title  = {ConCert: A Smart Contract Certification Framework in Coq},
  author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters},
  year   = {2019},
  eprint = {1907.10674},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1907.10674}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1907.10674.svg)](https://codeofpaper.com/paper/1907.10674)

Discussion