ABSTRACT. Programmatic interaction with a blockchain is often difficult. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees.

Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entrypoint of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.

ABSTRACT. In this short paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy+ algorithm. The algorithm is broken down to its essentials and represented as an automaton. The automaton models the various aspects of the algorithm: (i) the individual participant, referred to as a baker, (ii) how bakers communicate over the network (the mempool) and (iii) the overall network the bakers operate in. We also present a TLA+ implementation, which has proven to be useful for reasoning about this automaton and refining our documentation. The main goal of this work is to serve as a formal foundation for extracting intricate test scenarios and verifying invariants that Tenderbake's implementation should satisfy

ABSTRACT. In this work we present our research with the main goal of formally model and analyze the main blockchain consensus protocols. We have analyzed the protocol of the Bitcoin blockchain by using the PRISM probabilistic model checker. The probabilistic analysis of the model highlights how forks happen and how they depend on specific parameters of the protocol, such as the difficulty of the cryptopuzzles and the network communication delays. We also study the behaviour of networks with churn miners, which may leave the network and rejoin afterwards, and with different topologies.

ABSTRACT. The Diem blockchain, which was initiated in 2018 by Facebook, includes a novel programming language called Move for implementing smart contracts.  The correctness of Move programs is especially important because the blockchain will host large amounts of assets, those assets are managed by smart contracts, and because there is a history of large losses on other blockchains because of bugs in smart contracts. The Move language is designed to be as safe as we can make it, and it is accompanied by a formal specification and automatic verification tool, called the Move Prover.  The Diem Framework is the Move code that makes up the core logic of the Diem blockchain, managing accounts, payments, etc.  Extensive formal specifications have been written for the most important properties of the Framework, all of which can be formally verified by the Move Prover in less than 40 seconds per file.  Indeed, the framework is re-verified automatically in continuous integration whenever new code is submitted to Github. The entire blockchain implementation, including the Move language, virtual machine, the Move Prover, and near-final various Move modules are available on https://github.com/diem/diem.

This talk will be about the goals of the project and the most interesting insights we've had as of the time of the presentation.