LEVER - Verified, Playable Code Diffs

Paste a PR. Lever runs the real changed code in a sandbox, differential-tests old vs new & lets you pull on a playable microworld simulation of the difference or refuses honestly if it can't prove it.

Comment

Inspiration

An agent handed back a diff six hundred and sixty-seven lines, clean syntax, every test green and I realized I had no idea what it would actually do to a real system at 3am on a bad day. Not because I couldn't read the code. Reading code and knowing its behavior turned out to be two different skills, and only one of them was keeping up with how fast the agent could write.

That gap became a reframe: this isn't technical debt. It's cognitive debt every diff nobody truly understands is a small loan against a future incident, compounding silently because nothing forces you to pay it down today. Every existing tool did the same thing: describe the diff in prose, a claim with no evidence behind it, and I'd already watched language models confidently narrate behavior the code didn't actually have.

The question that drove the build: what would it take to make a falsifiable claim about a diff instead of a plausible one not "here's what this probably does," but "here's the real code, actually executing, and here's the measured proof it matches what you're seeing." And if we couldn't build that proof, say so, honestly, rather than show something reassuring and wrong.

What It Does

Your situation What Lever does
You paste a GitHub PR Resolves to two exact commits, checks out both versions into completely isolated environments
Lever prepares to test it Builds two harnesses byte-for-byte identical except which version of your code they import
Verification runs Executes the real code in a sandbox, differential-tests old vs. new across 100+ sampled inputs
Verification passes Opens a playable microworld already sitting on the most interesting divergence drag knobs, scrub a timeline, click straight through to the responsible line
Verification fails Refuses honestly, names the specific reason, never renders a fake result
You click the confidence badge Real stack trace, real sampled inputs, downloadable harness the claim, checkable in one click
You want to go further Swap the search objective to hunt for a specific unsafe input, generate a candidate for code that doesn't exist yet, or compose two PRs to catch bugs that only appear when they combine

Domain packs the same trust machinery, five different visual grammars:

Pack Renders as Proven on
Rate limiter Two overlaid curves / particle arena Hero 1, Hero 2
Permission Tappable access matrix Hero 3
Decision tree Union tree, fork ringed, unreached dimmed Hero 4
State machine Node graph, active state highlighted Real GitHub PR, live
Numeric fallback Generic x→y curve Always-satisfiable safety net

Also tested live, during the build, against a real pull request pulled straight from GitHub no special-casing, no fixture written in advance.

How We Built It

Eight-agent pipeline, spec-first, phase-gated each phase had to prove one fact real before the next was allowed to begin:

Agent Trigger Purpose
Intake PR / ref pair / demo Resolve to two commits, dual checkout
Triager Gate Checkout complete Static skip-check for no-op diffs, under 150ms
Scout Triager passes Entry point, dependency classification, reach-set scoping
Delta Analyst Scout completes Proposes thesis, knobs, observables
Harness Engineer Spec drafted Builds the byte-identical harness pair
Fidelity Verifier Harness built Byte-identity check → differential test → stability check → one confidence score
Adversary Verified Searches for maximum divergence, caches every point
World Director + Synthesizer Divergence found Picks visual grammar, renders it, enforces zero-anchored axes

Where the E2B sandbox runs - the "we actually ran it" guarantee

Every claim Lever makes is backed by real code executed inside an isolated E2B sandbox never on the host, never inferred from a summary. The sandbox is the trust layer: if it can't run, Lever degrades honestly instead of guessing.

The domain only ever talks to a SandboxRuntime port; the live adapter is E2BSandboxRuntime, and tests use FakeSandboxRuntime so no test touches the network. Real code executes in the sandbox at six points:

The orchestrator owns the sandbox lifecycle and converts any SandboxExecutionError into an honest degradation card. The Triager, Scout's static core, the Symmetrist math, the confidence statistics, and the rendering switch are pure deterministic code that never calls a sandbox or a model, by design.

Real problems Codex caught, not just implemented

What we found Real consequence How we caught it The fix
Confidence formula's normalization constant didn't match our own sample size Even a perfect result could never mathematically cross the "verified" threshold Ran real numbers through it a known-perfect case still scored "medium" Corrected the constant, reproved against that exact case live
Sandbox connections could be silently reused after a prior failure A pipeline could hang forever with zero error, mid-demo Only appeared under real, repeated live load never in isolated tests Fresh connection per attempt + explicit hard timeout
Harness-generation logic had one function name hardcoded from the first reference case A second, differently-shaped change crashed outright instead of degrading Pointed the pipeline at a new shape on purpose Pulled into a registry — every shape declares its own contract, unmatched shapes degrade honestly
Byte-identity check used one shared allowance across every comparison pair Could never actually catch a real mismatch, even if one existed Caught in review before spending a live verification call Per-pair justification, plus a test built to exercise the exact blind spot

Test suite

Suite Files Result
Backend (pytest) 39 129 passed, 1 skipped (live E2B test, safely skipped offline)
Frontend (Vitest) 16 38 passed
Total 55 167 passing

Challenges We Ran Into

Challenge What actually happened How we caught it The fix
A formula that could never succeed Even perfect agreement and perfect stability couldn't cross the verified threshold — bad arithmetic, not a coding bug Refused to trust the formula until real numbers were run through it Corrected the constants, reproved against the same case
A silent hang under real load A stale connection from an earlier failure could hang the whole pipeline forever, no error at all Only surfaced running the pipeline repeatedly, back to back, like a real user would Fresh connection lifecycle + hard timeout a hang is now loud, never invisible
Trusting our own story over the evidence Our working theory for one reference change was wrong the real, measured effect was a different, larger mechanism entirely Actually ran the search instead of reasoning about it Rewrote the explanation to match the measurement
Same failure, every new kind of code, at first The field the model needed was technically present but not genuinely inspectable Every new reference change hit it fresh, until we started checking for it first Made the real information visible in the code's own structure never a smarter prompt

Accomplishments That We're Proud Of

  • The core claim held real differential testing against real code, in a real sandbox proven before a single agent existed, true across every reference change, live
  • Four completely different shapes of code, same trust machinery, zero shortcuts
  • Verified a real GitHub PR we didn't build for, with no special-casing
  • Refuses as confidently as it verifies every dead end is named, never silent
  • Caught our own mistakes a broken formula, a hidden hang, a wrong assumption before anyone else had to
  • 167 passing tests, covering every agent and guardrail independently

What We Learned

  • Almost every dangerous failure looks exactly like success until you force yourself to check the real number
  • A formula that returns a number looks like it's working. A pipeline that finishes looks like it succeeded. Neither proves anything on its own.
  • That discipline, more than any single feature, is what this project actually is

What's Next

Deferred Why
Language support beyond Python, JavaScript, and TypeScript Real engineering lift - didn't want to rush into unsoundness to check a box
Second-order, indirect effect detection Static analysis genuinely can't see dynamic dispatch or reflection - unwilling to ship something that confidently guesses wrong
Mid-session harness modification without a full re-check Would quietly reopen the exact guarantee the system exists to protect

Built With

Share this project:

Updates