/scilla-coq

State-Transition Systems for Smart Contracts

Primary LanguageCoqBSD 2-Clause "Simplified" LicenseBSD-2-Clause

Smart Contract as Automata

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

Building Instructions

Requirements

We recommend installing the requirements via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

Building the project

make clean; make

Project Structure

  • 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;