SpecGuard: Proving a Task Is Broken Before the Agent Cheats
Param Biyani (MATS) and Krishnamurthy Dvijotham (Google DeepMind) present SpecGuard, which checks before an agent runs whether a coding task's description and its tests can both be satisfied, and produces a Lean 4 certificate when they cannot.
Ask this paper
Motivation. Agents given a task whose tests contradict the stated intent rarely flag the conflict. They edit tests or hard-code outputs, and in prior work have deleted a security defense to make a corrupted test pass.
Method. The task description and codebase are autoformalized into a Lean 4 specification, the tests are formalized independently, and the Lean kernel checks whether any implementation could satisfy both.
Results. On conflicted SWE-bench tasks SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1%. With GPT-5.6 Sol the conflict miss rate is 8.1%, against 39.8% for an LLM-judge baseline.
Failure source. Most misses come from aligning the two independently generated formalizations, not from proof checking.
Beyond benchmarks. The method also certifies naturally occurring test conflicts collected from real GitHub repositories. A certificate can be re-checked without trusting the models or the authors.
Abstract
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 this https URL.