Loading...

Synthetic
Minds

Build perfect DAPPS

How it works

Tech FAQs

Get early invite!
scroll down

We have built an automatic programmer

First release: June 2018!

Formal verification of smart contracts

Our formal verifier for Solidity will prove the correctness of your smart contracts. It automatically validates your business logic in the presence of every other contract that might exist on the blockchain, now and in the future. We have written a symbolic formal verifier for Solidity. It will soon be extended to support all other contract languages, across all blockchains.

Automatic programmer for smart contracts

Our automatic programmer will build user contracts for your smart contract. Observing your contract's interactions with users predicts its future behavior on the blockchain. A state-of-the-art program synthesizer powers this automatic programmer. It is the only system in existence that automatically writes provably correct smart contract code.

Smart contract "automated audits"

The synthesizer and formal verifier together perform automated audits of smart contracts. Validation using this automated duo are faster, cheaper, and more comprehensive than human auditors. By exploring every possible user contract, every possible interaction, under every possible blockchain state, they are able to find every interesting situation your contract might end up in (e.g., double spends, business logic failures, etc.)

Secure your Dapps

"Automated audits" for Dapps/smart contracts
1

Prove

Fully automated formal verifier for Solidity audits your contract.

2

Autocode

Use the automatic programmer to build "users" for your contract.

3

Simulate

Simulations evaluate your contract's interaction with the generated users.

Demo: Marketplace




Screencast
Demo: Marketplace
Solidity Source
Suppose you are building a market place that facilitates selling and buying data on the blockchain.
Demo: Marketplace
Formal verifier
"sm --prove" runs Synthetic Minds' formal verifier for Solidity, which performs an automatic audit of your contract.
Demo: Marketplace
Automatic Programmer
"sm --autocode" runs Synthetic Minds' automatic programmer that builds "users" for your contract, and if any interactions are suspect, it will send you the user's code for examination.
Demo: Marketplace
Auto-synthesized user
You can examine the generated "user" contracts that will be your contract's counter-party on the blockchain.
Demo: Marketplace
Simulate the interactions
You can also simulate the interaction between your contract and the generated user. Use this to improve your contract, until the automatic programmer cannot find any troublesome user. Then, your contract is secure to deploy.
Demo: DAO Root Cause




Screencast
Demo: DAO Root Cause
Solidity Source
The classic example of the root cause of the DAO vulnerability.
Demo: DAO Root Cause
Formal verifier
"sm --prove" runs the verifier. Without knowing the flawed pattern, and just by knowing the semantics of Solidity, the verifier is able to identify issues.
Demo: DAO Root Cause
Automatic Programmer
"sm --autocode" runs the synthesizer to generate the misbehaving user.
Demo: DAO Root Cause
Auto-synthesized user
The misbehaving auto-generated user exercises the classic re-entrant path.
Demo: DAO Root Cause
Simulate the interactions
Use "sm --simulate" with the synthesized user to understand the flaw.

Built on 10+ years of research

Rebuilt in 2018 to leverage recent advances

Formal verification

Smart contract languages are universal. It is more likely that your contract will double spend or violate business logic due to bugs in code, rather than attacks on the consensus.


We have built a source-level formal verifier for Ethereum's Solidity. It is built on prior work by the team that has over 800+ citations.

Learn more

Program synthesis

The current synthesizer includes a Solidity front- and back-end. Other blockchains, and their respective smart contract languages will be simple to add, and are on the roadmap.


The program synthesizer is a symbolic proof-based system that writes Solidity. It leverages work described in 11 peer-reviewed papers and patents, and a PhD.

Learn more

Blockchain semantics

Close to $0.5B have been lost due to unclear semantics of Solidity. Aside from experts most programmers will miss a few quirks. An automated programmer helps.


We compile Solidity into a non-EVM blockchain intermediate representation (BIR) that is perfect for formal analysis. Automated proofs of correctness and synthesis follow.

To be published soon

Roadmap

Generation -2: Formal verifier
Milestone: Apr 2018

Source-level formal verifier for Ethereum's Solidity.

Generation -1: Program synthesizer
Milestone: May 2018

Program synthesizer for Solidity.

Generation 0: "Anika"
Release: Jun 2018

Read and write Ethereum's Solidity for automated audits.

Generation 1
Expected Release: Oct 2018

4 orders of magnitude faster than Generation 0.

Generation 2
Expected Release: Dec 2018

Read and write all smart contract languages, across all blockchains.

Generation 3
Expected Release: Apr 2019

Decentralized program synthesizer.