BenFen选择Move语言的核心原因之一，就是其强大的原生安全性，特别是对形式化验证的支持。
什么是形式化验证？
形式化验证是一种通过数学方法来严格证明代码是否符合其预期规范的技术。与传统的单元测试（只能覆盖有限的场景）不同，形式化验证可以穷尽所有可能的输入和状态，从逻辑层面证明合约不存在某类漏洞。
形式化验证是一种通过数学方法来严格证明代码是否符合其预期规范的技术。与传统的单元测试（只能覆盖有限的场景）不同，形式化验证可以穷尽所有可能的输入和状态，从逻辑层面证明合约不存在某类漏洞。
BenFen如何应用？
-
Move Specification Language (MSL)：开发者可以使用MSL为自己的Move合约编写规范（如前提条件、后置条件和不变量）。
-
Move Prover：BenFen生态提供Move Prover等工具。开发者可以将自己的合约代码和规范输入Prover，Prover会像一个自动化的数学家一样，尝试证明代码在任何情况下都满足规范。如果找到反例，则证明存在漏洞。
通过鼓励和支持形式化验证，BenFen旨在帮助开发者在部署前发现并修复深层次的逻辑漏洞，从而从根本上提升整个生态系统的安全性。