  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.
