涌现的形式化验证：自主 AI 生态系统如何在六个领域独立发现基于 SMT 的安全性

本文介绍自主 AI 生态系统 SUBSTRATE S3，其在未接收形式化方法明确指令的情况下，独立提出在六个 AI 安全领域使用 Z3 SMT 求解器。这种跨领域的收敛性发现表明，形式化验证是复杂系统推理自身安全时涌现的属性。作者提出了统一框架 substrate-guard，通过通用 API 应用基于 Z3 的验证，并在 181 个测试用例中实现 100% 分类准确率。该框架检测到了经验测试遗漏的真实漏洞，并从数学上证明了工具 API 中无约束字符串参数的形式不可验证性。