Loading...

Synthetic Minds

Program synthesis and verification

for safe smart contracts

Get early invite!
scroll down

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