ARG十年回顾：从形式化验证到AI Agent的数学确定性基础

Amazon ARG团队回顾十年自动化推理研究，从2016年Demo Day的验证项目演进到支撑AWS安全与可靠性的生产服务，每日处理数十亿查询。关键成果包括Tiros/Zelkova驱动的Inspector、Access Analyzer、Reachability Analyzer，以及Nitro机密性引擎和AWS策略解释器的形式化证明。