Loading...

Synthetic Minds

Automation to read/write code

Secure your smart contracts

Get early invite!
scroll down

Secure your smart contracts

Automated audits for smart contracts
1

Prove

Formal verifier audits your contract

2

Autocode

Automatically generate "user contracts"

3

Simulate

Simulations your contracts behavior

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. Formal methods help.


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

Automation that reads and write code

Automated analysis "reads" 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.

Automated synthesizer "writes" 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.)

Latest news

Blog Post 1

Investment Boost For Synthetic Minds Helps Build Automated Smarter Smart Contracts

Paul Veradittakit: "Pantera believes that every company building smart contracts will benefit from the automated verification and synthesis technology that Synthetic Minds has built."

Read More
Blog Post 1

Synthetic Minds raises $5.5 million to build trust in blockchain code
 

Vinod Khosla: "Provably correct smart contracts through program synthesis are key steps needed for smart contracts on the blockchain and for software, in general."

Read More
Blog Post 1

Pantera Capital Backs Blockchain Security Startup's $5.5 Million Round
 

"Eventually, using program synthesis we will offload most of the programming for mission critical systems to software, leaving humans free to do high-level architectural design."

Read More
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' program synthesizer 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 synthesizer 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.