Agentic frameworks are the software layer through which AI agents act in the world. Existing safety methods intervene on the model and therefore remain conditional on unverifiable properties of learned behavior. We introduce containment verification, which locates safety guarantees in the agentic framework itself. Under havoc oracle semantics, the AI is modeled as an unconstrained oracle over the framework's typed action space, and the verified containment layer must enforce the boundary policy for every typed action value the AI can emit. For boundary-enforceable properties, expressed over modeled boundary events, action arguments, and state, we prove a universal guarantee by forward-simulation refinement and mechanize it in Dafny. We instantiate the paradigm by verifying PocketFlow, a minimalist agentic LLM framework, and use an agentic synthesis pipeline to generate the specification, operational model, and refinement proof under an information barrier against tautological specifications. To our knowledge, this is the first deductive formal verification of an agentic framework. The guarantee is independent of alignment because it quantifies over the framework's typed action boundary rather than over model behavior.
The Off-Support Barrier: Why Semantic Safety Constraints Are Not Learning-Problem Invariants, and What Follows for Prior Design, Containment, and Verification
A Survey of Safety and Trustworthiness of Deep Neural Networks: Verification, Testing, Adversarial Attack and Defence, and Interpretability
University of Liverpool（利物浦大学）；University of Oxford（牛津大学）；Lancaster University（兰卡斯特大学）；Defence Science and Technology Laboratory (Dstl)（国防科学技术实验室）；Queen’s University Belfast（贝尔法斯特女王大学）
Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations
Vanderbilt University（范德堡大学）
神经网络已被广泛用于解决复杂的现实问题。由于神经网络的复杂性、非线性和非凸性，对神经网络输出行为的形式安全保证将是其在安全关键系统中应用的关键，本文研究了一类由ReLU（Rectified Linear Unit）激活函数构成的神经网络的输出可达集计算和安全性验证问题.提出了一种逐层计算输出可达集的方法。计算公式化的形式，一组操作的多面体，它可以有效地应用与援助的多面体计算工具。基于输出可达集计算结果，可以通过检查由多面体的并集描述的不安全区域和输出可达集的交集来执行ReLU神经网络的安全性验证。一个随机生成的ReLU神经网络的数值例子表明本文开发的方法的有效性。
Internalizing Safety Understanding in Large Reasoning Models via Verification
National University of Singapore（国立新加坡大学）；University of Science and Technology of China（中国科学技术大学）；Shanghai Artificial Intelligence Laboratory（上海人工智能实验室）
Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes
The Institute of Statistical Mathematics（统计数学研究所）；Tohoku University（东北大学）；RIKEN AIP（理化学研究所人工智能中心）；CyberAgent；National Institute of Informatics（信息学国立研究所）
TriGuard: Testing Model Safety with Attribution Entropy, Verification, and Drift
Center for Data Science, New York University, New York, USA（数据科学中心，纽约大学，纽约，美国）；University of New Haven, Connecticut, USA（新罕布什尔大学，康涅狄格，美国）；Queens College, City University of New York, USA（皇后学院，纽约城市大学，美国）
Safety Testing LLM Agents at Scale: From Risk Discovery to Evidence-Grounded Verification
AntGroup（蚂蚁集团）；Zhejiang University（浙江大学）；Fudan University（复旦大学）；Alibaba Group（阿里巴巴集团）；Hunan Institute of Advanced Technology（湖南先进技术研究院）；Deakin University（迪肯大学）
A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation
University of Liverpool（利物浦大学）；Purple Mountain Laboratories（紫金山实验室）；Université Grenoble Alpes（格勒诺布尔阿尔卑斯大学）；The University of Manchester（曼彻斯特大学）；KU Leuven（鲁汶大学）
Self-Improving Safety Performance of Reinforcement Learning Based Driving with Black-Box Verification Algorithms
ITU Artificial Intelligence and Data Science Research Center（伊斯坦布尔技术大学人工智能与数据科学研究中心）；Department of Aeronautical Engineering（航空工程系）；Eatron Technologies（Eatron技术公司）；Department of Electronics and Communication Engineering（电子与通信工程系）；ITU Artificial Intelligence and Data Science Application and Research Center（伊斯坦布尔技术大学人工智能与数据科学应用与研究中心）；Department of Computer Engineering（计算机工程系）
