Scilla: a Smart Contract Intermediate-Level LAnguage
Ilya Sergey, Amrit Kumar, Aquinas Hobor

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Formal Methods in Verification · Logic, programming, and type systems
