Verification Is All You Need

Verification built into the delivery pipeline

A base artificial intelligence model can already write most of a feature correctly on the first try. The bottleneck comes afterwards: whether a human or an agent — the model carrying out a task — can show that the change is safe to merge. At Prover, a company built on formally proving that a design does what it claims, we did not want that decision to rest on instinct. We built verification into the pipeline that ships Prover Labs itself.

The name deliberately echoes Attention Is All You Need. That paper proposed one mechanism, applied consistently, in place of a collection of bespoke architecture. Our bet is smaller but just as literal: once a change can be verified mechanically and then in a real browser, there is no need for an elaborate trust ritual around the agent that wrote it. The verification must be good enough for its verdict to stand on its own.

What deterministic checks cannot see

Every change to Prover Lab goes through the same first gate — a check that must pass before the change can proceed. The command make check runs identically on a developer's machine and through continuous integration (CI). It is strict, inexpensive and suited to the mechanical checks that computers already perform well.

296 backend tests, plus ruff and mypy, on every push

9 frontend tests, eslint, feature-map check and production build

2 container images built, but not pushed, on every merge request

0 skip flags — a failed check remains a failure, not a TODO

These checks do not establish that the feature works. A database migration can apply cleanly while a form points at the wrong endpoint. A component can pass every type check while rendering a sign-in button that nobody can reach with a keyboard. Ruff does not watch a browser.

Rather than asking unit and snapshot tests to imitate that job, the second gate does what the first structurally cannot: it looks at the running product.

An independent witness, not a script

The second gate uses a fresh reviewer agent that did not write the change. It receives the request, the diff — the recorded differences introduced by the change — and a short behaviour contract for each affected feature, such as sign-in, notebook or ask-prover. The contract names the promised behaviour and the boundary worth distrusting, but it deliberately leaves the investigation to the agent rather than prescribing a script.

Scope is fail-closed: A path-to-feature map decides which contracts apply. Any unmapped path stops the run outright; there is no skip flag. Extending coverage means declaring the mapping rather than ignoring the path.
The instance is disposable: The reviewer drives a fully isolated application with its own ports, database and build output. It never touches a developer's running environment and cleans up after itself.
It drives a real browser: The reviewer controls Chromium through ARIA roles and accessible names — the same handles used by a screen-reader user. It batches steps for each feature to reduce the token cost, where tokens are the units of text processed by the model.
Evidence is curated, not dumped: The result includes one final snapshot and one screenshot per feature, plus a second, read-only view to confirm that any action changing data actually took effect. It does not produce a click-by-click transcript that would create another haystack to search.

A verdict cannot outlive its patch

A PASS that survives the next commit is worse than no verdict: it becomes a stamp that has stopped meaning anything. The verdict is therefore keyed to a stable git patch-id — an identifier derived from the branch diff — rather than to a commit hash, timestamp or person's word.

$ git diff origin/main..HEAD | git patch-id --stable
  7e67022896181728878fff62af0db8…  → .verify/<patch-id>.md

A local hook, an automatic check in the developer's Git workflow, looks for that file before git push or glab mr create can run. It fails closed: if it cannot determine the patch ID for any reason, it refuses to proceed rather than guessing.

Amending one line after the verdict changes the ID. The old PASS no longer applies, and the gate remains red until a fresh review covers the new diff. This hook is only an early, local workflow gate that the developer's own Git can see. GitLab cannot see an ignored file, so the CI gate is what protects main.

The framework had to pass its own bar

Adding a verification framework and treating the ceremony itself as the achievement would have been easy. Instead, the framework had to be the kind of change it would approve.

The merge request that introduced it removed UI unit tests, snapshot tests and the standing test suite for complete product flows. Those categories were expensive in tokens to write and maintain, while a real browser pass already covered them for a product of this size. What remained had to earn its place on every run.

The final cleanup commit alone removed 1,695 net lines from the framework and its documentation, reducing the whole merge request from 3,367 added lines to 1,672. Because that commit changed only verification tooling rather than the product, it did not require a fresh six-feature browser pass. The existing browser drive still covered the applicable product surface. Reusing a true verdict is not the same failure as reusing a stale one.

Trust is earned per diff, not per agent

Letting an agent open — and eventually merge — its own merge request does not require trusting the agent more. It requires trusting the gate more, while making that gate inexpensive enough to run on every change and strict enough for a green result to mean something.

The method combines deterministic checks for what can be proved mechanically, an independent reviewer driving a real browser for what only the running product can reveal, and a verdict that expires as soon as its diff changes. It does not depend on a bigger model. It narrows the gap between "the change looks right" and "the change is right."