ABSTRACT. Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed.

Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract.

As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once. This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.

ABSTRACT. Various smart contracts have been designed and deployed on blockchain platforms to enable cryptocurrency trading, leading to an ever expanding user base of decentralized exchange platforms (DEXs). Automated Market Maker contracts enable token exchange without the need of third party book-keeping. These contracts also serve as price oracles for other contracts, by using a mathematical formula to calculate token exchange rates based on token reserves. However, the price oracle mechanism is vulnerable to attacks both from programming errors and from mistakes in the financial model, and so far their complexity makes it difficult to formally verify them. We present a verified AMM contract and validate its financial model by proving a theorem about a lower bound on the cost of manipulation of the token prices to the attacker. The contract is implemented using the DeepSEA system, which ensures that the theorem applies to the actual EVM bytecode of the contract. This theorem could be used as proof of correctness for other contracts using the AMM, so this is a step towards a verified DeFi landscape.

ABSTRACT. Once you have invented money, you will find that you need a ledger to track who owns what --- along with an interface to that ledger so that users of your money can transact. On the Tezos blockchain this implies: a smart contract (distributed program), storing in its state a ledger to map ownership addresses to token quantities; along with standardised entrypoints to query and transact on accounts.

A bank does a similar job --- it maps account numbers to account quantities and permits users to transact --- but in return the bank demands trust, it incurs expense to maintain a centralised server and staff, it uses a proprietary interface ... and it may speculate using your money and/or display rent-seeking behaviour. A blockchain ledger is by design decentralised, inexpensive, open, and it won't just decide to bet your tokens on risky derivatives (unless you want it to).

The FA1.2 standard is an open standard for ledger-keeping smart contracts on the Tezos blockchain. Several FA1.2 implementations already exist.

Or do they? Is the standard sensible and complete? Are the implementations correct? And what are they implementations \emph{of}? The FA1.2 standard is written in English, a specification language favoured by wet human brains but notorious for its incompleteness and ambiguity when rendered into dry and unforgiving code.

In this paper we report on a formalisation of the FA1.2 standard as a Coq specification, and on a formal verification of three FA1.2-compliant smart contracts with respect to that specification. Errors were found and ambiguities were resolved; but also, there now exists a \emph{mathematically precise} and battle-tested specification of the FA1.2 ledger standard.

We will describe FA1.2 itself, outline the structure of the Coq theories --- which in itself captures some non-trivial and novel design decisions of the development --- and review the detailed verification of the implementations.

ABSTRACT. Algorand is a late-generation blockchain that features several interesting features, including high-scalability and a no-forking consensus protocol based on Proof-of-Stake. Besides this, Algorand features a complex transaction mechanisms, which supports both stateless and stateful smart contracts. Although this mechanism is already used in practice to develop industrial use cases, it is still largely unexplored by the research community. In this extended abstract we summarize our ongoing work on formal modelling of Algorand smart contracts.

ABSTRACT. Decentralized Finance (DeFi) has brought about decentralized applications which allow untrusted users to lend, borrow and exchange crypto-assets or crypto-derivatives. Many of such applications fulfill the role of markets or market makers, and thus feature complex, highly parametric incentive mechanisms to equilibrate interest rates or prices. This complexity makes the behaviour of DeFi archetypes difficult to understand and to predict: indeed, ineffective incentives and attacks could potentially lead to emergent unwanted behaviours. Reasoning about DeFi applications is made even harder by the lack of executable models of their behaviour: to precisely understand how users interact with DeFi instances, eventually one has to inspect their different implementations, where the incentive mechanisms are intertwined with low-level implementation details. To this end, we are developing new executable specifications of the DeFi archetypes lending pools and automatic market makers, allowing us to prove universal properties and precisely describe their interactions, vulnerabilities and attacks. In this presentation, we introduce this new line of research which aims to bridge the research communities of economic analysis and formal methods, paving the way for the development of formally secure, domain specific languages for DeFi.