OpenShell：用形式化方法约束 AI 代理权限

OpenShell 分享在大规模、长期运行 AI 代理场景下应用形式化方法的经验，讨论权限审查失效风险并演示如何用开源 Z3 库证明代理提出的策略变更在批准范围内。