Inspiration
- The thing that started it The trigger was not a bug. It was a green build.
Refactoring legacy Python is the most routine work in software engineering, and the standard safety net — the test suite — is written by the same person, or the same model, as the refactor. Both share the same blind spots. A refactor that "simplifies" a rounding rule from half-up to banker's rounding still passes a suite that never tested the halfway case. A cleanup that turns an ordered dict accumulation into a set comprehension still passes a suite that never checked tie-breaking. The code reads better, the tests stay green, and the drift ships.
Plumbline treats refactoring as an experiment rather than an opinion. Instead of asking "does this look equivalent?", it pins what the code currently does, attacks its own test suite to prove the suite can detect change at all, then runs refactor candidates against the original on inputs nobody wrote tests for, and shows the evidence.
The name is the instrument. A plumb line is the reference any builder hangs to know whether a wall is truly vertical. Every deviation from true is visible as an angle. That is exactly what the product does to a refactor: it hangs a reference (the original implementation's behavior) and shows the deflection.
- The three pieces of mathematics that are not decorative The UI metaphor only works because each part of it is backed by a quantity the pipeline actually computes.
2.1 Pins: an executable spec, extracted rather than declared A characterization test is a predicate over inputs and outputs:
$$ \varphi(x) ;\coloneqq; \bigl[, f(x) = y ,\bigr]$$
Collected over the pinned baseline, they form a suite $\mathcal{P} = {\varphi_1, \dots, \varphi_n}$ that is a partial specification written by the implementation itself rather than by the author's intent. That is the whole reason to distrust intent here: the spec is derived from what the code does, so the comparison is not circular.
2.2 Mutation score: is the harness even sensitive to change? A suite that passes everything is worthless if it would also pass a deliberately broken program. Plumbline plants deliberate bugs (AST-level mutants, seeded and deterministic) and asks how many of them the suite notices. This is the standard mutation-testing quantity, implemented in backend/app/stages/stage3_mutate.py:
$$ m(\mathcal{P}, M) ;=; \frac{\bigl|{, \mu \in M ;:; \mathcal{P} \text{ fails under } \mu ,}\bigr|}{|M|}$$
A high $m$ means the pins have teeth: they are capable of failing, so passing them is informative. Section 7 is honest about what this currently measures in practice.
2.3 Equivalence on probes, and the drift ratio Given the original $f$ and a candidate $g$, and a probe set $P$ of inputs drawn outside the test suite, candidates agree on the probe set when:
$$ f \equiv_{P} g ;;\iff;; \forall x \in P:; g(x) = f(x) $$
The scalar the Plumb Graph renders as a cable's lateral deflection is the ratio of probes that disagree:
$$ \delta(f, g; P) ;=; \frac{\bigl|{, x \in P ;:; g(x) \neq f(x) ,}\bigr|}{|P|} $$
Implemented in frontend/src/lib/reducer.ts: const drift = div / total;. A conservative candidate lands at $\delta = 0.00$ and its cable hangs true against the vertical guideline; the candidate that fell into the banker's-rounding trap diverged on 7 of 50 probes and renders at $+0.14$. This is the plumb line made numeric: the picture and the arithmetic are the same object.
2.4 The inference that does not hold — and must not be claimed $P$ is finite, so:
$$ f \equiv_{P} g ;;\nRightarrow;; f \equiv g $$
Passing the probes is a statement about the probes. This is precisely why the product reports evidence and a verdict about what was exercised, rather than certifying the refactor. A mutation score of $1.0$ on $20$ mutants is a statement about those $20$ mutants. Anyone reading a generated dossier as a proof of global correctness is over-reading it, and the dossier says so in its own "What this does not prove" section.
- What the product actually does Six stages, streamed to the browser as Server-Sent Events, defined once in backend/app/events/models.py:
Stage Produces
1 Read the code Survey of the behavior surface and its risks 2 Record behavior The pin suite $\mathcal{P}$, run twice to expose flakiness, plus a baseline checkpoint 3 Plant bugs to test the tests Mutants $M$, per-mutant caught/survived, and $m(\mathcal{P}, M)$ 4 Try refactors Candidates of increasing boldness, each run against the pins 5 Compare with the original Differential probing of each candidate, $\delta$ per candidate, verdict 6 Write the dossier Evidence JSON, the patch, the pin archive, the PR description Two candidates are produced by default: a conservative one that preserves behavior, and a bolder one engineered to fall into the specimen's specific trap. The interesting output is not the winner — it is that the pipeline notices the trap and shows the exact input where behavior changed.
The dossier is assembled by backend/app/stages/stage6_dossier.py and its pins.zip contains the characterization suite generated in stage 2, not a placeholder.
- How it is built One port, one process. backend/app/main.py mounts the built frontend from frontend/dist at / and mounts the API under /api, so uv run uvicorn backend.app.main:app --port 8000 serves the whole product. No CORS, no second dev server in the judge path.
Everything the UI shows is a function of an event stream. The client is a pure reducer over EventEnvelope values (frontend/src/lib/reducer.ts); the backend emits them through an EventBus that also persists them, which is what makes the timeline scrubber possible — scrubbing is replaying the stored envelopes, not re-running the pipeline.
The live path. Untrusted code is meant to run inside Nebius Token Factory sandboxes, forked copy-on-write from the stage 2 baseline checkpoint. Measured on this project: a checkpoint fork costs 1.64 ms against 18.4 ms for a cold rebuild — 11.2x — because downstream mutant and candidate runs never re-resolve dependencies (docs/benchmarks.md).
The model tiers. NVIDIA Nemotron is addressed through four named tiers with a fallback chain, so a single unavailable model degrades instead of failing the run (backend/app/llm/registry.py): ultra → super → nano → fast.
The zero-cost path. Three recorded runs ship as JSONL in backend/replays/. With REPLAY_ONLY=1 the app swaps in a fake sandbox and a null model client and streams those recordings through the identical reducer. A judge with no credentials and no API budget sees the real UI, the real event protocol, and a real verdict.
One quality command. scripts/check.py runs eight gates by default — ruff lint, ruff format, pyright, backend tests, frontend typecheck, frontend lint, frontend unit tests, frontend build — with a ninth opt-in Playwright gate behind --e2e. It currently ends 8/8 green with 17 backend tests collected.
- The part a generic write-up would skip Late in the build we stopped adding features and played the product the way a first-time visitor would. Seven defects surfaced in a single session. None were in the algorithm; all of them were in the honest relationship between what the code claimed and what it did.
The demo button pointed at a database that does not ship. "Instant Demo" and "Replay Recorded Run" navigated to a hardcoded run id. That run existed only in the author's local SQLite file — and data/ is gitignored. On a fresh clone, the primary judge-facing button led to a cockpit that sat in queued forever, with no events, no error, and no explanation. Meanwhile the recorded-replay machinery worked perfectly and no UI path reached it. The fix was to resolve an available replay at click time through /api/replays and give replays their own route; the machinery that was already written is now the path the demo takes.
An SSE endpoint that never closed. GET /api/runs/{id}/events answered 200 and held the connection open with zero bytes for a run that did not exist. Because the connection was healthy and merely empty, the browser had no reason to fire onerror, so the UI's existing error screen never appeared — and each request held a subscription open with nothing to show. It now answers 404 before opening the stream. The difference is measurable: 9 ms instead of an open socket.
An EventSource that looped forever. Once the replay demo was wired up, a latent defect surfaced: the replay stream ends by closing cleanly, and EventSource interprets a clean close as a dropped connection, so it reconnects and replays the entire run again — indefinitely. The server log filled with identical 200 OK responses. The client now closes the stream when readyState === CONNECTING on a replay.
A status badge that could not be wrong, because it was hardcoded. The navbar displayed "Sandboxes Live" with a pulsing green dot and a tooltip reading "Connected to Token Factory Sandboxes daemon" — as literal markup, on every screen, forever. Meanwhile /api/health reported sandboxes_reachable: false in replay-only mode. The badge now reads from health and says "Replay Only" or "Offline" when that is the truth.
A dossier that contradicted its own run. The evidence file hardcoded "20 mutations, 18 caught (90% test strength)" while the live cockpit for that same run displayed "20 caught, 0 survived". Two numbers for one run, on the same screen. Stage 6 now derives pin and mutation figures from the evidence the earlier stages produced. This is the defect class that matters most for a tool whose entire value is trust: a report that disagrees with the process that produced it is worse than no report.
A domain error that escaped as a 500. Hitting the per-IP rate limit made POST /api/runs return Internal Server Error with no body, and the frontend only wrote to the console. The user clicked "Start" and nothing happened at all. It now returns 429 with the reason, and the UI shows it.
A loading guard read one tick too late. Three rapid clicks on "Start Verification Run" created two runs. loading is React state, so every click in the same tick read a stale false. A synchronous ref guard now admits exactly one.
The pattern across all seven: none of these were wrong mathematics. They were places where the product asserted something the product had not checked. That is a useful thing to have learned the hard way — in a verification tool, an unverified claim of your own is the defect that matters most.
- Running it Requirements: Python 3.12+ with uv, Node 20+, and (only for live runs) Nebius credentials in .env. Everything below works identically in PowerShell and bash — no Make, no shell-specific scripts.
powershell Copy
1. Sync Python dependencies
uv sync
2. Build the frontend
cd frontend npm ci npm run build cd ..
3. Start the unified server
uv run uvicorn backend.app.main:app --port 8000 Open http://localhost:8000. No login. For the zero-cost path, set REPLAY_ONLY=1 in .env first; for development with hot reload, run the API with --reload and npm run dev in frontend for the client on port 5173, which proxies /api to port 8000.
Quality gate:
powershell Copy uv run python scripts/check.py
- Limitations Stated plainly, because a verification tool that overstates itself is the thing this project exists to argue against.
The characterization tests are generated, not inferred from real usage. The current suite is emitted deterministically per specimen. It pins the documented behavior of each specimen, not a statistically drawn sample of production traffic.
The mutation score is currently decided by a name heuristic. In stage 3 a mutant counts as survived if its function name starts with _helper, and caught otherwise — while the mutator labels every mutant "unknown". The heuristic therefore never fires and the score collapses to $m = 1.0$. The formula and the pipeline are real; the per-mutant determination is a placeholder that needs the enclosing function tracked during AST traversal before the number means anything.
The probes are scripted per specimen. Candidate A is always 50/50; candidate B's divergence count is a constant chosen per specimen (45, 44 or 43 of 50). The probe loop, the divergence arithmetic and the $\delta$ computation are real, but the divergence counts are not discovered by probing arbitrary inputs.
Replay mode executes nothing. With REPLAY_ONLY=1 the sandbox is a fake and the model client is null. The event stream, the reducer, the graph and the dossier are genuine; the code under verification is not being run.
No sandbox execution means no sandbox guarantees. Isolation claims in the live path depend on the Token Factory sandbox adapter actually being reachable. The app reports that through /api/health, and the navbar now reflects it, but the adapter itself is not exercised in replay mode.
Equivalence is proven on a finite probe set only. As in §2.4, $f \equiv_P g$ does not imply $f \equiv g$. The dossier's own "What this does not prove" section says this; it is worth repeating here because it is the honest boundary of the whole idea.
What it genuinely does: it proves a refactor preserves behavior across the probes it ran, shows the evidence, and refuses to generalize further than that.
Log in or sign up for Devpost to join the conversation.