Awesome Open Source
Awesome Open Source


Simplicity is a blockchain programming language designed as an alternative to Bitcoin script.

The language and implementation is still under development.


This project contains

  • A Haskell implementation of Simplicity's language semantics, type inference engine, serialization functions, and some example Simplicity code.
  • A Coq implementation of Simplicity's formal denotational and operational semantics.


Building with Nix

Software artifacts can be built using Nix.

  • To build the Haskell project, run nix-build -A haskell.
  • To use the Haskell project, try nix-shell -p "(import ./default.nix {}).haskellPackages.ghcWithPackages (pkgs: [pkgs.Simplicity])".
  • To build the Coq project, run nix-build -A coq.

Building without Nix

Building the Coq project

These instructions assume you start within the simplicity root directory of this repository.

Coq 8.12.0 is most easily installed via opam by following the instruction at

  1. Install opam using your distribution's package manager.
  2. opam init
  3. eval $(opam env)
  4. opam pin -j$(nproc) add coq 8.12.0
  5. opam install -j$(nproc) coqide # optional step

Next we use opam to install the CompCert dependency

  1. opam repo add coq-released
  2. opam install -j$(nproc) coq-compcert.3.7+8.12~coq_platform~open_source

While the VST dependency is available via opam, we need a custom build.

  1. wget -O - | tar -xvzf -
  2. cd VST-2.6
    1. make -j$(nproc) default_target sha
    2. make install
    3. install -d $(coqc -where)/user-contrib/sha
    4. install -m 0644 -t $(coqc -where)/user-contrib/sha sha/*.v sha/*.vo
    5. cd ..

Now we can build (and install) the Simplicity Coq library.

  1. cd Coq
    1. coq_makefile -f _CoqProject -o CoqMakefile
    2. make -f CoqMakefile -j$(nproc)
    3. make -f CoqMakefile install # optional


Detailed documentation can be found in the TeXmacs file. A recent PDF version can be found in the pdf branch.

Further Resources


Interested parties are welcome to join the Simplicity mailing list. Issues and pull-requests can be made through GitHub's interface.

Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
tcl (83