2016年，亚马逊成立自动化推理团队（ARG），其核心使命是将形式化验证技术从学术领域引入实际生产系统。如今，该团队构建的系统每天处理数十亿次查询，能够从数学层面证明AWS基础设施的正确性，而非仅依赖传统测试手段。
ARG的发展历程
ARG最初开发了Tiros和Zelkova等基础工具，这些工具后来演变为面向用户的正式服务，包括IAM访问分析器、Amazon Inspector和可达性分析器。目前，数百万客户依赖这些服务进行安全分析和网络分析，并获得数学层面的正确性保障。
关键基础设施的形式化验证
ARG通过形式化验证和SMT求解器，证明了多项关键AWS基础设施的正确性，包括：Nitro隔离引擎、密码学实现，以及每秒处理十亿次API调用的授权引擎。这意味着这些系统的安全性和正确性不再只是"经过测试"，而是经过数学证明的。
从研究到规模化落地
ARG的十年历程展示了一条清晰的路径：将严谨的学术方法转化为可大规模部署的工程实践。形式化验证不再是象牙塔中的理论工具，而是支撑全球云基础设施安全运行的核心技术之一。
Q&A
Q1：亚马逊自动化推理团队（ARG）是做什么的？
A：ARG成立于2016年，专注于将形式化验证技术引入AWS生产系统。与传统测试不同，形式化验证能从数学层面证明系统的正确性。该团队每天处理数十亿次查询，为AWS的安全性和可靠性提供数学保障。
Q2：IAM访问分析器和可达性分析器是怎么工作的？
A：这两项服务由ARG的Zelkova和Tiros等底层工具演化而来，利用SMT求解器对权限策略和网络可达性进行形式化分析。用户可以获得数学层面的安全与网络分析结论，而非仅依赖经验性测试结果，目前已有数百万AWS客户在使用。
Q3：Nitro隔离引擎的正确性是如何被证明的？
A：ARG通过形式化验证方法，对Nitro隔离引擎的设计和实现进行了数学证明，确保其隔离属性在所有可能的执行路径下均成立。这与传统的功能测试不同，形式化验证能覆盖穷举的状态空间，从根本上排除特定类别的安全漏洞。
