智能合约是区块链上执行各种商业活动的软件程序。近年研究发现了一类新的“机器不可审计”漏洞，它们源于源代码未能满足底层交易上下文。现有检测方法需要人工理解交易逻辑并手动推理不同上下文来源（即模态），例如代码和描述预期交易行为的自然语言。为了自动化检测这类漏洞，本文提出了SmartInv，一个准确且高效的智能合约不变量推断框架。核心洞见在于，智能合约的预期行为（通过不变量指定）依赖于跨模态信息的理解和推理，如源代码和自然语言。作者提出了一种新的基础模型微调和提示策略——Tier of Thought (ToT)，用于在智能合约的多个模态间进行推理并生成不变量。SmartInv随后通过检查这些生成不变量的违反情况来定位潜在漏洞。实验评估基于过去2.5年（2021年1月1日至2023年5月31日）导致财务损失的真实世界智能合约漏洞，结果表明SmartInv能生成有效不变量，准确定位“机器不可审计”漏洞，共发现119个零日漏洞。从中采样了8个漏洞报告给相应开发者，其中6个被迅速修复，5个被确认为“高严重性”。该研究展示了利用多模态大模型自动推理智能合约安全性的可行性和有效性。