[Introduction](https://verity.md/docs) [Quickstart](https://verity.md/docs/quickstart) [Authentication](https://verity.md/docs/authentication) [How it works](https://verity.md/docs/how-it-works) [Moments](https://verity.md/docs/moments) [Formal verification](https://verity.md/docs/formal) [Findings & verdicts](https://verity.md/docs/findings) [The Standard](https://verity.md/docs/standard) [Memory](https://verity.md/docs/memory) [Org knowledge](https://verity.md/docs/org-knowledge) [Token telemetry & cost](https://verity.md/docs/cost) [The dashboard](https://verity.md/docs/dashboard) [CLI & commands](https://verity.md/docs/cli) [Files & configuration](https://verity.md/docs/files) [Security & privacy](https://verity.md/docs/security) [Troubleshooting](https://verity.md/docs/troubleshooting)

Concepts

# Formal verification

At push, Verity can build a small Lean 4 model of one risky function in the change, search every interleaving of its actions, and replay any failure on the real code. It is a bug finder, not a proof of the program — and most pushes never get one.

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:

1. **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).
2. **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.
3. **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.
4. **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](https://verity.md/docs/moments) 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](https://verity.md/docs/security).

## 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](https://verity.md/docs/findings) handles apply.

[Previous Moments](https://verity.md/docs/moments) [Next Findings & verdicts](https://verity.md/docs/findings)

Source: https://verity.md/docs/formal