先区分审计对象
区块链审计方法相关术语如何理解，首先取决于检查对象。智能合约审计关注程序逻辑、权限和状态变化；链上记录验证关注交易是否被收录、输入是否有效以及区块是否符合规则。两者可以配合，但不能相互替代。
以太坊开发者安全文档介绍了合约测试、静态与动态分析、形式化验证及独立审查；比特币开发者指南说明了交易、区块与共识验证机制。这些概念各有适用范围，不能直接套用于所有区块链系统。
静态分析、动态分析与模糊测试
静态分析通过代码结构和执行路径寻找问题，无须实际执行被检查的合约。动态分析则运行程序并观察结果；模糊测试属于动态分析，通过生成大量不同输入探索异常行为。单元测试检查预设用例，属性测试关注多种输入下某项规则是否持续成立。
理解这些方法时，应同时看检查覆盖范围。例如，正常操作测试通过，只说明这些用例符合预期；权限异常、边界输入或连续调用产生的状态变化，仍需相应检查。工具告警也需要结合业务逻辑判断。
不变量与形式化验证
不变量是要求在指定执行边界持续成立的性质，例如受限操作只能由获授权账户完成。形式化验证把安全要求写成精确规范，再证明程序模型满足规范。其结论受规范、模型和假设约束，不能扩大为整个系统绝无漏洞。
阅读验证结论时，可以追问：证明了什么性质，覆盖了哪些操作，依赖哪些外部条件？如果规范遗漏关键要求，即使证明成立，也不能回答被遗漏的安全问题。
权限控制与异常处理
访问控制规定谁能执行敏感操作，常见方式包括所有者权限、角色分工和多签授权。require通常用于检查输入或前置条件，assert用于检查预期始终成立的内部性质，revert用于主动中止执行并回滚相关状态变更。
审计需要检查这些机制是否落实到每个敏感入口。拥有角色分工或多签配置，并不自动说明权限设计合理，还要看授权范围、管理关系及实际生效条件。
哈希、默克尔证明与UTXO
比特币通过区块哈希链接历史记录，默克尔树支持核验交易是否被包含在某个区块中。UTXO指未花费交易输出，普通交易的输入引用可用输出；共识规则则规定节点如何判断交易和区块有效。
默克尔包含证明回答的是收录问题，不能单独证明交易符合全部规则。UTXO检查适用于相应交易模型，也不能直接替代智能合约的状态与权限检查。
常见问题：通过审计是否代表安全
审计是针对一定范围的检查，其价值在于发现问题并提供可核查的依据。阅读报告时，应关注检查对象、采用的方法、发现的问题及修复复查情况。独立审查、测试和形式化验证可以互补；任何单一方法都不应被理解为对所有潜在风险的保证。