SCILLA

Safe-By-Design Smart Contract Language

Documentation Try it! GitHub

About

Scilla, short for Smart Contract Intermediate-Level Language, is an intermediate-level smart contract language being developed for Zilliqa. Scilla has been designed as a principled language with smart contract safety in mind.

Scilla imposes a structure on smart contracts that will make applications less vulnerable to attacks by eliminating certain known vulnerabilities directly at the language-level. Furthermore, the principled structure of Scilla will make applications inherently more secure and amenable to formal verification.

The language is being developed hand-in-hand with formalization of its semantics and its embedding into the Coq proof assistant — a state-of-the art tool for mechanized proofs about properties of programs.

Tutorial



Let's start with a look at the classical "HelloWorld" contract.
Libraries



A Scilla contract may come with some helper libraries that declare purely functional components of a contract.

A library is declared in the preamble of a contract using the keyword library followed by the name of the library.
HelloWorld contract code has a function one_msg in the library and two global constants.

Standard libraries shipped with the language can be added using the keyword import followed by the name of the library.

Code Snippet: "HelloWorld"

(***************************************)
(*         Associated library          *)
(***************************************)

library HelloWorld

let one_msg =
 fun (msg : Message) =>
 let nil_msg = Nil {Message} in
 Cons {Message} msg nil_msg

let not_owner_code  = Int32 1
let set_hello_code  = Int32 2


(Im)mutable variables



Scilla contracts have two types of state variables: mutable and immutable.

Immutable variables are those that get initialized at the time of contract creation. Once initialized, their values cannot be changed. HelloWorld has one immutable variable named owner.

Mutable variables are those whose value will change even after the contract has been created. HelloWorld has one mutable variable named welcome_msg.

contd...

(**************************************)
(*       The contract definition      *)
(**************************************)


contract HelloWorld
(owner: Address)

field welcome_msg : String = ""



Step 3: Functions aka Transitions








Transitions are functions that change the value of mutable variables and can communicate with other contracts.

The first transition, setHello, takes a String as input, updates welcome_msg and informs the caller of the success/failure.

The second transition, getHello, simply sends out a message to the caller with the current value of welcome_msg.

contd...

transition setHello (msg : String)
 is_owner = builtin eq owner _sender;
 match is_owner with
 | False =>
   msg = {_tag : "Main"; _recipient :            _sender; _amount : Uint128 0;            code : not_owner_code};
   msgs = one_msg msg;
   send msgs
 | True =>
   welcome_msg := msg;
   msg = {_tag : "Main"; _recipient :            _sender; _amount : Uint128 0;            code : set_hello_code};
   msgs = one_msg msg;
   send msgs
 end
end

transition getHello ()
   r <- welcome_msg;
   msg = {_tag : "Main"; _recipient :            _sender; _amount : Uint128 0;            msg : r};
   msgs = one_msg msg;
   send msgs
end

Resources



To learn more about Scilla, you can avail of the following resources:
Read The Docs
Full documentation on Scilla to get an in-depth understanding
Scilla Technical Paper
Technical paper outlining key designing principles of Scilla
Scilla Design Story: Part 1
Blog post on "Why do we need a new language?"

Formal Verification


The language is being developed hand-in-hand with formalization of its semantics and its embedding into the Coq proof assistant — a state-of-the art tool for mechanized proofs about properties of programs. Coq is based on advanced dependently-typed theory and features a large set of mathematical libraries. It has been successfully applied previously to implement certified (i.e., fully mechanically verified) compilers, concurrent and distributed applications, including blockchains among others.

Formal methods can provide static guarantees on contracts before they get irrevocably committed to the blockchain. Guarantees typically come in the form of proofs of safety and liveness properties. Safety properties are invariants that are valid over the lifetime of a contract and hence capture the fact that nothing should go wrong. Liveness properties are those that ensure that certain action may eventually happen over the lifetime of a contract.

Dev Tools



Developers can make avail of multiple tools to make the process of coding and testing Scilla contracts easier.
Savant IDE
A standalone IDE to quickly write and test Scilla contracts in a simulated blockchain environment.
Zilliqa-JS Library
A Javascript library to interact with the Zilliqa network nodes - Create wallets, deploy contracts and invoke transitions.
Develop Apps
JSON-RPC APIs for developing dapps.

FAQ


Why a new smart contract language?

Incidents with smart contracts over the last few years (such as the DAO and Parity hacks)  have shown that implemented operational semantics of smart contract languages often admit rather subtle behaviour that diverge from the intuitive understanding of the language in the minds of contract developers.

In order to prevent such incidents to recur, it is required to have a safe-by-design smart contract language that is both expressive and tractable.


What does Scilla offer?

Scilla aims to be a structured  and principled smart contract language that is expressive enough to develop “interesting“ dapps while ensuring the safety of contracts and enabling formal reasoning about contract behavior.

Contracts in Scilla are structured as communicating automata, i.e., a state machine that takes input from the external environment, performs some purely mathematical computations, change the state of the system and at the end (if needed) communicate with other contracts.


What are the high-level design principles in Scilla?

The language adopts certain design principles to make contracts tractable and hence easier to reason about:

Separation between computation and communication:  Every in-contract computation (e.g., changing its balance or computing a value of a function) is implemented as a standalone, atomic transition, i.e., without involving any other parties. Whenever such involvement is required (e.g., for transferring control to another party), a transition would end, with an explicit communication, by means of sending and receiving messages.

Separation between effectful and pure computations: Any in-contract computation happening within a transition has to terminate, and have a predictable effect on the state of the contract and the execution.

Separation between invocation and chained contract calls: The language only allows tail-calls, i.e., every call to an external function (i.e., another contract) has to be done as the absolutely last instruction.

What is the current state of development of Scilla?

Scilla is under active research and development. The language comes with an interpreter that can be used to try our Scilla contracts. Check the tutorial section to learn more.

Is Scilla specific to Zilliqa?

No, while Scilla was designed in the context of Zilliqa, it is not agnostic to the underlying blockchain platform and hence can be used with any other blockchain.

Get Involved



Once you've covered the basics and are ready to move forward, do get involved in the development of Scilla.
Scilla's Github Repo
Contribute to Scilla project.
Gitter
Join the developer community conversations!
Jobs
Join Zilliqa - The team behind Scilla.