该论文提出了一种结合大型语言模型（LLMs）与形式化方法的智能合约验证新框架。当前智能合约验证面临两大挑战：自然语言表达的属性内在存在歧义，且LLM的答案缺乏正确性保证。作者通过两个创新点同时解决这些问题：1）设计了一种扩展Solidity语言的正式规范语言，支持抽象类型，使得属性表达无歧义；2）开发了一个工作流，将LLM与类型检查和具体执行相结合，自动生成并验证违规见证（即反例）。其核心思想是将规范编码为包含存在量化抽象类型变量的Solidity测试；通过为这些变量实例化具体值（符合正确类型），测试将转换为可执行的反例（概念验证），直观展示属性为何被违反。作者将该流程实现为工具Neuroforger，并在来自文献的智能合约验证数据集上实验评估，获得了有前景的结果，证明了其在真实场景中的潜在适用性。本文适合对智能合约安全、形式化验证及LLM应用感兴趣的读者。