本文提出一种自动形式化（autoformalization）流水线，旨在将智能体指令转化为“策略即代码”（Policy-as-Code），以在高风险领域中实现正式的策略执行。现有方法主要分为两类：一是基于概率性护栏（如微调分类器、提示引导），这类方法无法提供形式化保证；二是手工编写的符号化策略执行，但难以扩展到真实业务策略的广泛定义。该流水线利用基于LLM的生成器-评论家循环（generator-critic loop），将智能体提示、MCP工具描述以及自然语言策略文档自动翻译为使用Cedar策略语言编写的正式验证策略。在MedAgentBench基准上，自动形式化策略对源自然语言规范的覆盖范围显著超过先前工作中手工编写的符号化执行。该方法的核心贡献在于：通过自动形式化弥合了自然语言策略与形式化验证之间的鸿沟，使得非专家也能为智能体行为定义可验证的约束，而无需手工编码或形式化方法专业知识。实验证明，该流水线生成的策略在覆盖率和正确性上均优于手工基线，为智能体安全提供了一种可扩展、可验证的解决方案。