本系列文档翻译版权归FireStack团队所有，转载请注明来源。
智能合约通过一种去中心化的、拜占庭容错的分布式账本，很好地展现了区块链的计算形式。智能合约的出现，让开发者构建去中心化应用（Dapps）成为可能。这些应用的运行及业务逻辑皆可编写为智能合约，放到去中心化的区块链网络上运行。
在去中心化网络上运行应用，使得受信任中心节点、定制化服务器的需求不复存在。如今智能合约非常受欢迎，在诸如众筹、游戏、去中心化外汇交易、支付处理等场景，智能合约有力推动了现实经济环境的发展。
然而，从过去几年的经历来看，智能合约的实践催生了一些游走于边缘的行为，这偏离了开发人员关于智能合约的最初理念。这种分歧导致了对智能合约的重大攻击事件，例如对DAO合约和Parity钱包的攻击。正因为区块链的不可篡改性，智能合约无法获得直接升级修复，这使得问题日益严重。因此，确保智能合约的安全运行至关重要。
事实证明，形式化证明和模型检验等方法在提高其他领域的软件系统的安全性方面是非常有效的。所以我们很自然会想到将其用于探索提高智能合约的可读性和安全性。另外，这些方法也能严格保证合约行为的规范性。
然而，使用现有语言（如Solidity）在形式化证明工具上进行应用并不是一件容易的事。因为典型的图灵完备语言有其非常特别的表达形式。诚然，在让语言更易于理解、易于验证、易于表达三者之间是存在着权衡的。例如，比特币的脚本语言具有易于理解的特点，并且对有状态对象不作处理。而图灵完备的语言（如Solidity）具有易于表达的特点。
Scilla是一种新的（中级水平的）智能合约，旨在同时实现易于表达的形式及可追踪性。基于前述有关合约行为的论证，Scilla设定的设计原理如下：
计算与通信的分离
Scilla中的合约会被构造为通信自动机：每个合约内计算（例如改变账户余额或运算函数值）会通过一种具有独立原子性转换（transition）的过程来实现。也就是说，这个过程不涉及到第三方。每当进行类似操作时（例如，向第三方转移控制权），转换（transition）会通过发送/接收消息这种显式通信来表示结束。自动机架构使得区块链上的通信（如发送/接收资金和消息）能直接解决某类合约纠纷（如transitions），这种清晰、合理的机制有利于撰写合约及保护不动产。
有效性和纯计算之间的分离
转换（transition）中发生的任何合约内计算必须可终止，并且合约状态和执行过程可预测。为了实现这一目标，Scilla从函数式编程思想中取其精华，将纯表达式（如原生数据类型和映射）、不完全本地状态管理（如读/写合约字段）和区块链反射（如读取当前区块编号）区分开来。通过介于纯语言和不纯语言之间交叉语义的严谨设计，Scilla确保了许多合约转换（如进程和类型保护）的基本性质不变，同时让它们适合通过独立工具进行交互式和/或自动化验证。
调用与持续之间的分离
合约构建作为一种自动化通信系统，它是一种仅允许尾调用的计算模型，即每次对外部函数（如另一个合约）的调用都必须是最后的完成指令。
