Main Goal

FRESCO (Formal Verification of Tezos Smart Contracts) is a project generously funded by Tezos Foundation that includes two Ph.D. theses. The main goal of this project is to explore tools for the static analysis of smart contracts in programming languages such as Michelson, as well as focus on formal verification techniques and support for machine-checked smart contracts using proof assistants like Why3 and Coq.

From this goal derive two lines of work (two Ph.D. theses) that focus on:

formal verification of smart contracts;
static analysis of smart contracts.

Static Analysis of Tezos Smart Contracts

Focused on static analysis of smart contracts, this line of work aims at developing methods and tools to automatically analyse, infer and verify certain properties of smart contracts.

This line of work will carry on a study of common problems and characteristics of smart contracts in order to develop the tools and techniques to infer and detect such properties.

As a target of these tool, any smart contract written in Michelson (or other future low-level like languages) should be supported.

Formal Verification of Tezos Smart Contracts

This line of work focuses on formally verifying the functional correctness of Michelson written smart contracts.

In order to have realistic correctness results about smart contracts, we intend to provide formal models for the virtual machine, as well as to the blockchain.

This means devising formal operational semantics, memory models, and compilation schemes.