# ConCert: A Smart Contract Certification Framework in Coq

## TL;DR

ConCert introduces a novel framework for embedding and verifying smart contracts in Coq, combining deep and shallow embeddings through meta-programming, enabling formal verification of blockchain contracts.

## Contribution

It presents a new embedding approach in Coq for smart contracts, linking deep and shallow embeddings with a soundness theorem, facilitating formal reasoning.

## Key findings

- Verified properties of a crowdfunding contract
- Connected deep and shallow embeddings via soundness theorem
- Formalized smart contract execution in Coq

## 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.