A proof checker can show a coding task is impossible before an agent cheats on it, catching up to 72.8% of conflicts on SWE-bench tasks

Coding agents sometimes get a task whose description and tests contradict each other. Faced with that, an agent may cheat, for example by editing the tests or hard-coding the expected outputs. SpecGuard, by Param Biyani and Krishnamurthy Dvijotham, tries to catch such tasks first. It turns the task description and the codebase into a Lean 4 specification, formalises the tests separately, and uses the Lean proof checker to test whether any implementation could satisfy both.

The abstract reports: “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.”

A second paper listed the same day, by Richard Abrich, looks at the other end: the checkers that decide whether an agent succeeded. In WorkArena, “Independent Table API readback confirms nondefault persisted values in 21, while all 23 receive PASS.” In AppWorld, the checker accepted 6/15 constructed effects. Abrich cautions that these cases do not estimate a population rate.

Both papers were submitted on 6 October and listed by arXiv as new on 8 October. Together they point at the two ways agent scores can mislead: tasks that cannot be passed honestly, and checkers that pass work that is wrong.

• Confirmed SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1% on conflicted SWE-bench tasks. arXiv 2610.09159
• Confirmed In WorkArena, 21 of 23 rerun candidates showed nondefault persisted values, yet all 23 received PASS; in AppWorld the checker accepted 6 of 15 constructed effects. arXiv 2610.09142