Counterexample

A coding agent that breaks your code before your interviewer does: Nemotron writes an oracle and adversarial input generators, then you get a minimal counterexample and a re-attacked fix.

Comment

Inspiration

"All tests pass" is where most coding help stops, and it is exactly where interviewers and code reviewers start. A strong interviewer does not rerun your examples. They look for the one input you did not think of: the empty array, the value at 2^31 − 1, the coin system where greedy fails, the graph with a negative edge. We build interview-prep tools (AlgoCracked), and we wanted an agent that does that part of the job: it does not write the code, it breaks it, and it proves the break with a minimal input. The same need shows up every day with AI-written code: it looks right, passes the obvious cases, and fails on the input nobody tried.

What it does

Paste a problem and a solution (your interview answer, or code an AI wrote) and press Attack.

  1. Understand. The problem becomes a typed spec of its parameters and constraints. When the statement relies on outside facts, or the user ticks Research the web, Tavily fetches the official sources: the problem's constraints, and the documentation of APIs the code calls that have a well-known trap (JavaScript's sort() without a comparator, Python's banker's round()). Every fact is cited in the trace. When the code calls such an API and research is off, the trace suggests turning it on.
  2. Build an oracle. Nemotron 3 Ultra writes a slow but obviously-correct brute force. It must reproduce the statement's examples before it is trusted; otherwise the verdict is "oracle unreliable" and no bug is claimed.
  3. Attack. Nemotron 3 Super designs adversarial input generators (not test cases) in a typed JSON DSL: bounds, duplicates, overflow, worst-case sizes, deep chains. They run alongside deterministic families: bounded-exhaustive small inputs and EvalPlus-style mutants.
  4. Run. The solution and the oracle run on up to a few hundred inputs before the first counterexample (hundreds to over a thousand when nothing breaks), and the fix on hundreds to over a thousand more (thousands of sandbox runs in all), in a sandbox (any Judge0-compatible API, or our own hardened sandbox).
  5. Confirm and shrink. A mismatch counts only once it reproduces alone on a fresh run. Delta debugging then shrinks it to a minimal counterexample, for example solve([2, 5], 6): expected 3, got -1.
  6. Explain and fix. Ultra explains the bug in two sentences and proposes a fix. The whole attack is re-run on the fix before it is called fixed.
  7. Report. A live trace shows every model call (which model, why, tokens, cost, latency) and every run. A "Why Ultra here, Super there" panel shows the cost of each step, and a share link carries the report in the URL.

How we built it

  • Nebius Token Factory and NVIDIA Nemotron. Every model call goes through Token Factory's OpenAI-compatible API. We route by the cost of being wrong:
    • Nemotron 3 Ultra handles the oracle and the root cause, where a mistake means a false alarm or a wrong fix.
    • Nemotron 3 Super handles generator design and research summaries, which are cheap to try and checked by a validator.
    • The benchmark compares this routing against Ultra everywhere.
  • Nebius AI Cloud. The attacked code runs in our own Judge0-compatible sandbox (sandbox/). It is designed to deploy as a Nebius Serverless AI endpoint, so that the models run on Token Factory and the code they attack runs on Nebius AI Cloud (until it is deployed there, the sandbox runs from the same Docker image locally or behind any Judge0-compatible endpoint). Each run is isolated:
    • its own unprivileged uid;
    • a seccomp filter that denies network sockets and IPC;
    • resource limits;
    • a kill-all afterwards.
  • Tavily searches the problem's sources and the documentation of risky APIs the code calls. A fact such as MDN's "numbers are converted to strings, '80' comes before '9'" becomes a generator family that breaks a merge sorted with plain sort().
  • Safety by construction.
    • Model-written generators are interpreted, never executed, and every value they produce is bounded and checked against the problem's constraints.
    • Every external input (API body, model answers, Token Factory, Tavily and Judge0 responses) is schema-validated with zod.
    • Network calls have timeouts, bounded retries with backoff and idempotency keys.
    • Each attack has budgets for model calls, sandbox runs and wall clock.
    • Per-IP rate limits and a daily spend cap protect the public demo.
  • Next.js and TypeScript (strict) for the UI and the streaming API, a deterministic replay provider so the whole agent runs in tests and for judges without keys, and over 600 tests:
    • unit tests;
    • fast-check property tests;
    • integration tests;
    • a replay end-to-end test;
    • a Playwright browser smoke test.

Challenges we ran into

  • False alarms are worse than misses. A correct binary search looked broken under a loaded sandbox. We now confirm every mismatch alone in a fresh process before claiming it. A failure that only appears after earlier calls is reported as "order-dependent" (the solution keeps state), never as flaky.
  • Judge0 has one time limit per submission. We size batches so every input keeps its full limit inside the 15 s CPU cap, and blame a timeout on an input only after it times out alone.
  • Exact answers. Integers past 2^53 lose digits in JavaScript, so an overflow in the last digit would go unnoticed. We compare them by their exact digits.
  • Hostile inputs. Pasted code and model-written specs can try to freeze a server. Every generator, shrinker and parser step is bounded, and repeated hostile audits (more than 35 rounds by 29 October) found and fixed more than 150 issues.
  • No keys in the build environment. The build sandbox had no Token Factory or Tavily key (and at first no network route to Token Factory), so we built a replay provider and recorded every friction point in docs/FRICTION.md.

Accomplishments that we're proud of

  • 38 of 38 known bugs found, 0 false alarms on 16 correct solutions, across 13 problems in Python and JavaScript, with every fix verified by re-attack (replay mode: hand-written stand-ins for the model answers, real execution).
  • Where the models matter, measured honestly. On 8 "hard tier" bugs that only show at worst-case sizes or on specific structure (exponential backtracking, overflow on a long chain), the model-designed families find 8 of 8. Both ablations find 0 of 8: one without model families, and one with examples plus 1,000 random inputs. We wrote those stand-in families knowing the bug classes, and say so; the live run measures whether Super writes them itself.
  • Routing costs about half. Routed Ultra + Super costs about half as much as Ultra everywhere ($0.0882 against $0.1725 for all 54 solutions, estimated from replayed token counts at third-party list prices of $1/$3 and $0.30/$0.90 per million tokens) with the same results. Its time to the first counterexample is shorter too (median 5.5 s against 11.3 s), but in replay mode that latency is simulated from each model's decode speed, so only the live benchmark can confirm it.
  • Counterexamples a person can read: solve([0], 0), solve(2147483647), solve("baab").

What we learned

  • Generators beat test cases. A model is much better at describing what kind of input breaks code than at writing the one input that does, and a typed DSL makes that description safe to run.
  • Small inputs find most bugs (the small-scope hypothesis). On the base tier, the deterministic families (exhaustive small inputs, mutations and random inputs) found all 30 bugs without the models, so the models earn their cost on the hard ones.
  • An honest verdict needs a trustworthy oracle. Making the oracle pass the examples first, and saying "evidence, not proof" when nothing breaks, matters more than any clever generator.

What's next

  • Deploy the sandbox as a Nebius Serverless AI endpoint and publish the live benchmark.
  • A GitHub app that attacks AI-written functions in a pull request before merge.
  • More problem families: floating point, interactive problems and data-structure APIs.

Built With

Share this project:

Updates

Submission history