Source code of the Ergo smart contracts with compilation, testing, and formal verification tooling.

Certified(ErgoScala):

• Assets Atomic Exchange src , verified properties
• Crowd Funding src, verified properties
• ICO Funding src, verified properties

ErgoScript:

• DEX with limit orders and partial matching src docs

Certified contracts are written in ErgoScala (a subset of Scala, compiled with ErgoScala compiler) and have their properties verified using formal verification with Stainless.

• Install Z3 SMT solver from https://github.com/Z3Prover/z3

Subclass SigmaContract in the verified-contracts project and put a contract code in a method. The first parameter has to be ctx: Context, and subsequent parameters may be contract parameters. The return value has to be SigmaProp. Make the first line of the contract code import ctx._ to improve readability.

See DEX buy order for an example.

Create a subclass (object) of the class with contract code to make an "instance" method to compile the contract's code. It'll invoke the compiler (macros) and returns a compiled contract with embedded contract parameters. Create a method with parameters from the contract (without the Context parameter) and invoke ErgoContractCompiler.compile. See DEX buy order for an example. Mark this method with @ignore annotation to hide it from Stainless.

Call the "instance" method in another module/project, and it'll return 'ErgoContract'(compiled contract). Call ErgoContract.scalaFunc to run the contract with given Context. See DEX buy order for an example.

Verification is done using Stainless. Create a subclass(object) of the class where you put contracts (as methods). Use a method for each property you want to verify. Put pre-conditions in require() call, call the contract, and verify post-conditions. See DEX buy order verified properties for an example.