# SpecGuard: Proving a Task Is Broken Before the Agent Cheats

arXiv: https://arxiv.org/abs/2610.09159 · HTML: https://mlsanity.com/paper/2610.09159/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 28 of its 38 references that are in the map.
- First posted on arXiv 6 Oct 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 28 of 28)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscation](https://mlsanity.com/paper/2503.11926/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [LEVER: Learning to Verify Language-to-Code Generation with Execution](https://mlsanity.com/paper/2302.08468/) (2023)
- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [Natural Emergent Misalignment from Reward Hacking in Production RL](https://mlsanity.com/paper/2511.18397/) (2025)
- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [ImpossibleBench: Measuring LLMs' Propensity of Exploiting Test Cases](https://mlsanity.com/paper/2510.20270/) (2025)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [EvilGenie: A Reward Hacking Benchmark](https://mlsanity.com/paper/2511.21654/) (2025)
- [SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents](https://mlsanity.com/paper/2605.21384/) (2026)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [MalSkillBench: A Runtime-Verified Benchmark of Malicious Agent Skills](https://mlsanity.com/paper/2606.07131/) (2026)
- [Benchmarking Reward Hack Detection in Code Environments via Contrastive Analysis](https://mlsanity.com/paper/2601.20103/) (2026)
- [Monitoring Emergent Reward Hacking During Generation via Internal Activations](https://mlsanity.com/paper/2603.04069/) (2026)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [Agentproof: Static Verification of Agent Workflow Graphs](https://mlsanity.com/paper/2603.20356/) (2026)
- [The Verification Horizon: No Silver Bullet for Coding Agent Rewards](https://mlsanity.com/paper/2606.26300/) (2026)
- [Semia: Auditing Agent Skills via Constraint-Guided Representation Synthesis](https://mlsanity.com/paper/2605.00314/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents](https://mlsanity.com/paper/2607.22868/) (2026)
- [SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?](https://mlsanity.com/paper/2609.21190/) (2026)

## Abstract (arXiv)

As autonomous coding agents get increasingly deployed, the risk that accidental or adversarially injected misspecifications in tasks lead to dangerous agent behavior is critical to address. Prior work has shown that agents given such tasks rarely flag the conflict and instead cheat, editing tests or hard-coding expected outputs, and the actions taken to cheat can cause real damage, such as deleting a security defense to make a corrupted test pass. It remains unclear whether such conflicts can be established with independently verifiable evidence before the agent acts. We present SpecGuard, which detects and formally certifies these conflicts between task intent and tests. Given only the task description and codebase, SpecGuard autoformalizes the intended behaviour into a Lean 4 specification. The tests are formalized independently, and the Lean kernel checks whether any implementation could satisfy both formalizations, producing a machine-checked certificate when none can. On conflicted SWE-bench tasks, SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1%, with a nearly five-fold lower conflict miss rate than model-based judgment. SpecGuard provides a pre-execution safety check that identifies reward-hacking opportunities through formal certification of task-level conflicts, before any agent behavior is observed. Our code is available at https://github.com/prmbiy/specguard.