收录解读
self-evolving agents 这条线越来越强，但大多数框架只关心 planner 能否自动生成和改写 agent program，几乎不对 autonomy 带来的安全性、约束遵守和 correctness 给出形式保证。一旦这些程序在未见输入上自动执行，这个缺口就会直接变成 reliability 和 security 风险。
SEVerA 的核心推进，是把 agentic code generation 改写成带 hard constraints 的学习问题，并用 Formally Guarded Generative Models 为每次生成调用加 formal output contract。每个 generative call 都由 rejection sampler 和 verified fallback 包住，于是 planner 搜索、verification 证明和 learning 优化可以组合起来：软目标继续优化，但硬约束始终不被违反。
它值得正式收录，因为这条路线把 formal methods 真正接到了 self-evolving agents 的核心循环里，而不是做外围 guardrail。对安全 agent synthesis、tool-using agents 和可验证的 self-improvement，这是一条很清晰的 durable pattern。
它暂时不升到更高一级，原因在于当前 formal contract 的表达能力和任务覆盖还有限，主要验证也集中在 Dafny、symbolic math 和 policy-compliant tool use。它非常强，但还没证明自己会成为更广 agent synthesis 的默认接口。