模型检查

智能合约形式化验证是通过数学模型和逻辑规范确保合约安全性的关键技术。它采用模型检查、定理证明和符号执行等方法，验证合约是否符合预定义的高级规范（如安全性和活性）和低级规范（如霍尔属性）。相比传统测试，形式化验证能提供数学证明级别的安全保障，有效检测溢出、重入等漏洞。尽管存在人力成本高、规范编写复杂等挑战，但该技术对处理高价值、不可变合约至关重要。主流工具包括Certora Prover、Solidity SMTChecker和Manticore等，覆盖规范语言、程序验证和符号执行等场景。