Scilla: a Smart Contract Intermediate-Level LAnguage

TL;DR

Scilla is an intermediate-level language designed for verified smart contracts, enabling formal verification and safe interaction patterns by separating communication and programming components.

Contribution

The paper introduces Scilla's automata-based model and its use as a target for high-level languages to facilitate formal verification of smart contracts.

Findings

Automata-based model simplifies verification processes

Scilla enables formal safety and temporal property verification

Separation of communication and programming enhances contract safety

Abstract

This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.