Not every push is checked

The formal phase runs for one function per push at most, and only when the push touches something that looks worth it: a file the history says has been fixed before, a shape that tends to hide bugs (a check followed by a write, a retry, money, auth, a transaction, a cache), and a ranking score above the bar. A push of documentation, tests, configuration or plain code stops in under a second with a named reason. If you never see a formal result, that is usually the phase saying there was nothing worth modelling — not that it is broken.

What a model is

A model abstracts one function: its state (a balance, a set of ids, a flag), the actions that change it (a call, a retry, a second caller arriving, a crash between two writes), and a handful of properties — promises the code should keep. The checker explores every sequence of actions up to a bound and, when a property breaks, returns the shortest sequence that breaks it. That trace is a fact about the model. Whether it is a fact about your code is what the replay decides.

Models are written by the Verity service (the same independent model that reviews your changes), checked with Lean on your machine against a small precompiled library, and never committed: they live under .verity/proofs/, which ignores itself. The bug report and the fix are what reach your team, not the model.

Lean runs only in a .verity/proofs/ that this machine made. If git tracks any file in it, or its path goes through a symlink, Lean could load prebuilt files that the repository supplies. The phase then does not run Lean and reports the skip workspace-untrusted. To fix it, untrack the files with git rm -r --cached .verity/proofs, or remove the symlink.

Which functions get a model

Selection is a step of its own, and it is deliberately narrow:

Eligible files. Source files in the push — not tests, fixtures, vendored or generated code. A function qualifies when it has two or more effects (writes, calls out, state it keeps), or two risky shapes, or touches a critical domain (money, a transaction, auth).
Signals from history and text. Fix commits touching the file, churn, fix density, and how many risky shapes the text shows, each capped so volume cannot dominate.
A cheap ranking call scores each candidate on hazard, criticality and how error-prone the shape is, names the one function to model, and the properties worth stating. The ranking may re-order and annotate; it can never hide a candidate.
The bar. Only a candidate scoring 0.70 or above whose function the push actually touched is modelled. Functions over 300 lines are skipped. A model that already held for a function is not rebuilt while the push changes only logging, comments or whitespace.

The five structural rules

Properties come from two places. Structural properties come from a fixed catalogue of five rules and need no intent — they are true of correct code in any domain. Intent properties come only from something a human wrote: a comment, a docstring, a type, the words you type after /verity-prove.

Rule	The promise	The bug it finds
`conservation`	Money, stock and counts add up across every path.	A refund that credits without debiting; a seat reserved twice.
`once`	The same identified input — an event, message, delivery or request id — delivered or retried twice takes effect once.	A webhook that charges twice on redelivery; a seed that runs twice under two concurrent starts.
`no-lost-update`	Two concurrent writers never silently drop one another's write.	A read-modify-write on a counter; a cache refreshed by two callers.
`fail-closed`	An error in an access decision never grants access; a failed operation is never reported as done.	A permission check that allows on timeout; a sync marked complete after its request failed.
`progress`	Nothing is left waiting forever.	A state machine with a state no transition leaves.

Every property must say what it rests on — one of the five rules, or a line of the code's own words (L12: if (existsSync(path) && !force) return), checked on your machine against the real line. A property that rests on nothing is sent back to the model once, then dropped. The dashboard shows the basis beside each promise — the rule, or the line number; the line's words never leave your machine — so you can see which are the code's claims and which are the catalogue's.

The replay: when a counterexample becomes a finding

A counterexample in the model is not evidence about your code until it is replayed on the real function. The replay runs in a disposable container with no network: the real function is copied in verbatim, its I/O is stubbed, and the failing trace is driven against it. Two checks decide whether the answer counts, neither of which trusts the model's prose: the harness must have executed, and at least 80% of the function's significant lines must appear in what was run.

Verdict	Means	Effect on the push
Reproduced	The real code did what the model said.	Blocks, as a high finding — the only formal outcome that can.
Diverged	The real code did not do what the model said. The model was wrong; the code held.	None. Shown on the coverage line.
Unverified	The replay did not meet the evidence bar.	None. Counts for nothing.
Model only	Not replayed — out of time or budget.	None. Not evidence about the code.

A reproduced counterexample blocks only when the file it is about is in the push. A human can accept the risk with verity prove waive <file> --reason "…"; the waive binds to the file's exact bytes and returns when they change. The other rules of the git moment apply unchanged: the phase has a hard deadline inside the push's 180 seconds, and a phase that cannot finish is a named skip, never a silent allow.

Languages

Stage	Languages
Files that can be candidates	TypeScript, JavaScript, Python, Go, Rust, Java, Kotlin, Ruby, C#, Scala, Swift, PHP, Elixir
Files the code map can read (function extents, effects, callers)	TypeScript, TSX, JavaScript, Python, Go, Java
Files whose counterexamples can be replayed — and so can block	TypeScript, JavaScript and Python

A push in any other language stops before a model is paid for, with the reason replay-unsupported: without a replay, a model could only ever warn, and a warning about a model is not something the gate acts on. On demand (/verity-prove), a model can still be written and checked for any candidate language; you replay it by hand.

Turning it on and off

Formal verification is on for a new project. verity init turns it on, says so, and does not ask. A project Verity set up before keeps its setting: a re-run of init never turns it on, and an off stays off.

Init also starts the Lean 4 download in the background, once per machine: about 800 MB to download, about 2.7 GB on disk. Until Lean is ready, a push skips the phase and says so. The gate decision does not change:

verity · pre-push

  formal: skipped (no-toolchain: Lean installing, 63%)

Init does not start the download in CI, with VERITY_NO_LEAN=1, or when the disk has too little free space. Run verity lean install yourself then. Where Lean has no release for the machine, the formal check at push is skipped.

terminal

verity lean status            # is Lean ready? shows the background download's progress
verity lean install           # install it now (≈800 MB download, 2.7 GB on disk)
verity config formal off      # turn it off for this checkout
verity config formal push     # turn it back on

VERITY_GIT_MOMENT_FORMAL=push|off overrides .verity/config.json for one command. The phase also needs a Verity login. Two server-side switches can only turn it off: the Standard's process_constraints.git_moment_formal: off, and the Formal verification admin feature flag, per repository, org or globally. A push then reports the skip disabled-by-server.

On demand

/verity-prove in Claude Code runs the same machinery when you have a worry: “can the webhook double-charge on a retry?” The skill ranks candidates, confirms with you which function to model — a model is a claim about what code means, and only its owner can say if it is worth checking — writes and checks the model, and replays counterexamples. Nothing on this path blocks a commit or a push. The CLI exposes each step: verity prove candidates, generate, check, replay, and verity prove auto for the whole push-time phase run by hand.

Costs and caps

Per push: one function, up to three rounds to a compiling model, at most three counterexamples replayed in parallel, $1 at most.
Per repository per UTC day: five models, $5, twenty replays — enforced by the service from its own ledger, not by a file on your machine.
Per hour: 60 rankings, 20 model generations, 10 replays.
Time: the phase must finish inside the push review's 180 seconds; a model check has 120 s, a replay up to 240 s.

What the dashboard shows

When an admin has switched Formal in dashboard on for a repository, each push's phase appears as a record beside the review it ran with — in Runs, on the run page, and on the repository's Formal page:

the function chosen, its file and lines, its score, and why in numbers — commits, fix commits, the risky shapes counted; every other candidate ranked the same way;
the model's name and how many rounds it took to compile;
each promise by its id, what it rests on (a rule, or the number of the line it was read from), and its result to the bound;
each counterexample: the trace as a chain of action names, the replay verdict, and whether it held the push or was waived;
when nothing ran, the reason — no changed function scored above the bar, the daily cap was spent, counterexamples cannot be replayed for this language;
tokens, cost and duration.

What is, and is not, stored

The record is metadata about the phase. The function's source, the Lean model, the replay harness and the container's output are never stored; they exist for the length of the call. Nor is any prose: the record is identifiers, paths, line numbers and counts. A promise is its id, a trace is its action names, a basis is a line number, and why a function was chosen is a set of counts. The words the model wrote — the promise as it stated it, the ranker's reasons, the replay judge's sentence — stay in your terminal and your local log. What leaves your machine during the phase: the chosen function's source and up to three related excerpts, sent to the Verity service and, for a replay, into OpenAI's container — the same runtime the agent review uses. See Security & privacy.

Reading the terminal

verity · pre-push

  formal: SeedRunner on src/seed.ts#runSeed (2 rounds) · seed_once REPRODUCED · no_partial holds · 96 s · $0.31
  src/seed.ts:3   Formal: runSeed breaks "the seed runs at most once" — reproduced on the real code   [formal-counterexample]  high
      Trace: runSeed → runSeed. Replay: both calls passed the existsSync guard and posted 6 nodes.

  formal: skipped (no-candidate: no changed function scored above the bar)

The first block is a push that was held; the last line is what most pushes print. The finding's pattern id is always formal-counterexample and its source is formal, so the usual feedback and waive handles apply.