# ConCert: A Smart Contract Certification Framework in Coq

arXiv: https://arxiv.org/abs/1907.10674 · HTML: https://mlsanity.com/paper/1907.10674/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jul 2019.

## Built on by (most cited first, 1 of 1)

- [Multi-Agent Collaborative Fuzzing with Continuous Reflection for Smart Contracts Vulnerability Detection](https://mlsanity.com/paper/2511.12164/) (2025)

## Abstract (arXiv)

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.