Formal verifier audits your contract
Automatically generate "user contracts"
Simulates your contract's behavior
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
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
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
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.
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.
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.)
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
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
"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