**Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization**

> AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promising path: an agent generates code together with a machine-checked proof, guaranteeing that the code satisfies a formal specification. However, there is no guarantee that the formal spec itself matches the user's intent. In this work, we st...

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-05-28 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2605.26457)