本文详细介绍了形式化验证（formal verification）的过程及其在智能合约中的应用，强调了与单元测试的互补关系，以及如何利用Halmos工具简化形式化验证的实施。文中分析了正式验证的挑战、规范的编写开销及其在ERC721A智能合约中的案例，展示了通过符号测试实现高效验证的重要性。
Daejun Park