Smart Contract as Automata

State-Transition Systems for Smart Contracts: semantics and properties.

Building Instructions

We recommend installing the requirements via opam:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fcsl-pcm

make clean; make -j

Core/Automata2.v - definition of the automata-based language semantics;
Contracts/Puzzle.v - a simple puzzle-solving game contract and its properties;
Contracts/Crowdfunding.v - the Crowdfunding contract and its properties;