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.)
Fully automated formal verifier for Solidity
audits your contract.
Use the automatic programmer to build "users"
for your contract.
Simulations evaluate your contract's
interaction with the generated users.
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. 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
Source-level formal verifier for Ethereum's Solidity.
Program synthesizer for Solidity.
Read and write Ethereum's Solidity for automated audits.
4 orders of magnitude faster than Generation 0.
Read and write all smart contract languages, across all blockchains.
Decentralized program synthesizer.