形式化验证如何检查智能合约？它的基础流程是什么？

形式化验证是一种基于数学推理的智能合约安全检测方法，通过将合约代码逻辑与预期行为转化为数学语句，使用自动化工具穷举所有可能执行路径，证明合约是否满足功能正确性、安全属性和不变式等要求。与传统测试只能证明错误存在不同，形式化验证能够证明合约在