BenFen选择Move作为其智能合约的编程语言，以从根本上保障链上资产与应用的安全。Move是一种专为数字资产设计的、具备形式化验证能力的静态类型语言。
核心安全特性：
-
资源模型：Move的核心特性是“资源（Resource）”。资源在代码层面不能被复制或意外销毁，只能在程序存储位置之间进行移动，这从根本上杜绝了重入攻击和资产凭空消失等漏洞。
-
类型安全：严格的类型系统能在编译时捕获大量潜在错误。
-
形式化验证：BenFen提供Move Prover等工具，允许开发者通过数学方法严格证明其合约代码的正确性，极大提升了合约的可靠性。
-
标准库：为简化开发，BenFen提供了一个包含40多个常用模块（如账户、交易、数学计算等）的、经过形式化验证的智能合约标准库。