Scilla: a Smart Contract Intermediate-Level LAnguage

Ilya Sergey, Amrit Kumar, Aquinas Hobor
1/2/2018
cs.PL

Official code: pirapira/ethereum-formal-verification-overview (295 stars, last commit 2022-03-24).

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.

View on arXivView PDF

Code Implementations(1)

pirapira/ethereum-formal-verification-overviewOfficial100%

The start page about my efforts around smart contract verification

29524Oct 9, 20164 years ago

Similar Papers

Vandal: A Scalable Security Analysis Framework for Smart Contracts

86% match1 repo1672018

Logical foundations of Smart Contracts

85% match2025

Flint for Safer Smart Contracts

85% match1 repo2452019

Efficacy of Various Large Language Models in Generating Smart Contracts

84% match2024

SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

83% match2025

LLMs as verification oracles for Solidity

83% match2025

Cite this paper

@article{sergey2018scilla,
  title  = {Scilla: a Smart Contract Intermediate-Level LAnguage},
  author = {Ilya Sergey and Amrit Kumar and Aquinas Hobor},
  year   = {2018},
  eprint = {1801.00687},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1801.00687}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1801.00687.svg)](https://codeofpaper.com/paper/1801.00687)

Discussion