Tezos（特所思）作为著名的 PoS 公链，其亮点并不仅仅只是 Staking，Tezos 的形式化验证特征同样也是其主要技术亮点之一。形式化验证能让 DeFi 的安全性方面如虎添翼，让用户对资金的智能合约安全更加有信心。

形式化验证方法和 DeFi 安全

DeFi 的爆发式增长吸引了不少开发者，著名的 DeFi 协议如 Compound、Uniswap、Syntheix 累计收获了上亿美元的资金。但是，DeFi 存在一个重大漏洞：安全性。

这个漏洞的代价是昂贵的，它给一些区块链项目（比如以太坊）的网络效应带来了负面的影响。过去几个月被攻击的 DeFi 项目就包括 Curve.fi、Lendf.Me、PegNet 等，其损失从数十万美元到数千万美元不等。tBTC 在上线几天后通过自查及时发现了 bug 并冻结了存币，避免了一场灾难。

而对于注重安全性的 DeFi 开发者来说，Tezos 的形式化验证方案能够在加强安全性的同时赋能 DeFi 应用。

在传统互联网应用中，如果服务器被黑客攻击，只需要对服务器端用户数据进行回滚就可以挽回用户损失。因此，重视用户体验的传统互联网应用可以以牺牲安全性换取速度和功能上的快速迭代。然而在 DeFi 应用中，由于区块链的不可篡改性，智能合约一旦上线并出现安全隐患，对用户造成的损失是巨大且不可挽回的。

因此，DeFi 应用开发的过程需要用大量的测试和昂贵的审计以获取足够的安全性，而反过来会牺牲迭代的速度，影响了产品的易用性。并且，因为安全审计的价格昂贵，很多开发者并没有能力发起 DeFi 应用。

区块链开发人员目前仍然是稀缺的，导致人工审计的成本非常高昂。因此越来越多地使用机器辅助验证是目前的趋势，而机器辅助审计中的形式化验证方法更是确保安全性的不二法宝。

形式化验证指的是用数学中的形式化方法对算法的性质进行证明或证伪，方法有两种：

一种是模型检验，即把系统所有可能的状态列出并进行一一检验，此种方法全自动化但只适合小型系统；

另一种是演绎验证，首先把系统代码标记成抽象数学模型，然后对定理进行证明，此种方法适合大型系统，但是首先需要人工将系统的运作方法转换成验证系统可以理解的语言。

形式化验证方法在很长一段时间里，由于其成本较高昂，主要应用于学术、国防军工、航空航天等领域，在商业领域应用较少。由于传统互联网应用与区块链应用的运行环境有着本质的不同，其开发流程也应当相应地进行调整，其中最关键点在于安全验证环节的投入比例.

函数式语言在公链领域的应用

许多区块链项目为了保证安全性，在底层架构、虚拟机或智能合约的语言方面，选择了函数式语言，如 Ocaml、Haskell、Erlang 等。函数式语言由于其严格的变量类型定义和编译检验，以及拥有较好的形式化验证工具链（比如 CoQ ），在安全领域拥有很好的口碑。常见过程式语言编写的代码，一般必须重新用函数式语言标记方能进行形式化验证。

我们看到，在以上项目中，Tezos 支持的智能合约高级语言的种类最丰富，不仅包括 Pascal, Ocaml, Haskell 等多种函数式语言，也包括了 Python 这一应用普遍的语言。而 Cardano、Aeternity 都需要开发者学习一门新的函数式语言，使得开发门槛变得较高。

Michelson 语言的安全特性

在智能合约语言的设计上，Tezos 采用了一种取长补短的创新方案。Tezos 的智能合约底层采用基于 Ocaml 的 Michelson 语言，而开发者实际接触的是 Python 等高级语言，并不需要了解 Michelson 语言本身。如此以来，可以结合 Michelson 语言更好的安全性与可审计性，与 Python 等高级语言的易于编程性。

Michelson 在架构上对标的是以太坊 EVM ，与 EVM 相比其相似之处有

1）是一种 stack 语言

2）使用链上存储

3）采用 gas 费用模型

4）图灵完备

Michelson 与 EVM 的主要区别是，

1）静态类型

所有进入 Michelson 智能合约的数据，都需要明确定义其类型。避免了跟类型不匹配有关的程序 bug ，如浮点溢出、除以 0 等。

2）原子计算

一个 Michelson 智能合约必须完成执行后才能调用其它智能合约。这一点避免了以太坊上经常发生的 re-entrancy 攻击(如著名的 DAO 攻击）。

3）明确的调用失败

执行期发生的失败只有三种，明确失败（用 FAILWITH 语句处理）、gas 耗尽、数量溢出。这一点避免了以太坊上常出现的隐含模代数、错误指令、stack 溢出等类型的常见执行期攻击。

4）严格的语义

大小写、空格、短行都有严格规范的要求，让代码审计变得更方便。

可以看到 Michelson 相比 EVM 在安全上有诸多的改进，可以更好地抵御以太坊上经常出现的攻击类型。

SmartPy 开发工具包

Tezos 上的 Dapp 开发者并不需要掌握 Michelson 语言 。这是因为开发者可以使用基于 Python 的 SmartPy SDK ，并将 Python 代码写的智能合约编译成 Michelson 语言。因此 Dapp 开发者只需要会 Python 就可以轻松上手。

SmartPy是一个Python 库，而 SmartPy.io 让用户能够在一个浏览器中执行 Python 脚本。Smartpy 的官方网站提供了一个在线编辑器(https://smartpy.io/demo/)，Dapp 开发者可以直接用 Python 编写代码并编译成 Michelson 智能合约，然后部署到 Tezos 主网上。其使用界面设计相比以太坊的 Remix 在线编辑器更简洁明了，非常容易上手。Smartpy 还自带了一些现成的开发模版，方便开发者参考学习。

SmartPy.io 的界面如下。屏幕左侧区域是代码编写区，开发者可以轻松地使用 Python 来写入并编辑合约的代码。Smartpy 不需要像 Remix 一样分两步编译和执行，按一下代码区上方的执行按钮就一步搞定，非常方便。执行结果立马就可以在屏幕右侧显示出来，包括合约调用的入口、存储状态、编译的 Michelson 代码等。

除了在线编辑器，SmartPy 还有一个命令行版本 SmartPyBasic ，让开发者在本地环境也可以编译运行 SmartPy 代码。

部署的智能合约可以用 SmartPy Contract Explorer 进行查看，合约的当前状态和历史操作都一览无余。

目前 SmartPy 已经支持 Python 常见的许多功能，如本地变量，变量类型判断，Lambda 函数等。少数不支持的功能如 array，可以用 map 来代替。这也就意味着学习 SmartPy 不需要投入很多的时间和精力，开发者可以专注于实现更好的功能。