OpenShell团队分享了在AI智能体控制中应用形式化方法的研究成果。针对多智能体系统中权限管理难以扩展的问题，团队使用Z3 SMT求解器对策略进行形式化建模，能够自动证明提议的策略变更是否超出既定权限范围，从而防止智能体通过权限组合绕过安全控制。