The CTO Adjoint gave a technical talk about formal verification of smart contracts. Adjoint offers a smart contract platform and distributed ledger solutions designed to improve efficiency, security, and compliance in modern finance. Stephen defines smart contracts as executable programs that run on top of an immutable distributed database whose inputs and outputs are maintained globally consistent by a distributed consensus protocol. For a more detail look at Stephen’s thoughts on formal verification look at the work Adjoint are doing and read his blog post.
The most developed and well-known of platforms for deploying smart contracts is Ethereum. Ethereum is a public blockchain that embeds a Turing-complete virtual machine which uses a scripting language called Solidity. The code of any given smart contract is deployed by its owner and anyone on the network can interact with it. Stephen argues that smart contracts are extremely difficult to debug and analyse as it stands using current schools of thought. A crucial question therefore moving forward is ‘How do we know what the code will do before we run it?” While the answer to such a question may be obvious to those familiar with the literature of programming language semantics and software verification, projects in Solidity are making expensive mistakes due to a lack of tools for software verification of smart contracts.
Below you can find transcript of the talk and a Q&A session with other participants.