Formal verification
Finds the order of events that breaks your code.
Some bugs pass review because every line looks right. They show up only when two requests arrive together, a retry lands twice, or a call fails quietly. At push, Verity models one risky function in Lean, tries every order of its steps, and runs the one that fails on your real code.
1. Model
Verity writes a small formal model of one risky function, and the rule it must keep.
10 of 10 orders triedOne breaks the rule
2. Search
It searches the possible orders and outcomes of the function's steps, up to a limit, for one that breaks the rule.
3. Replay
It runs that case on the function's real code, with stand-ins for what the function calls. Only a failure that reproduces can block a push.
The promises it checks
| Rule | The promise | A bug it finds |
|---|---|---|
| Conservation | Money, stock and counts add up on every path. | A refund that credits without debiting |
| Once | The same event, delivered or retried twice, takes effect once. | A webhook that charges twice on redelivery |
| No lost update | Two writers never silently drop each other's write. | A counter updated by two requests at once |
| Fail closed | An error never grants access, and a failure is never reported as done. | A permission check that allows on timeout |
| Progress | Nothing is left waiting forever. | A state that no step ever leaves |
Verity also states promises from your code's own words: a comment, a docstring, a type, or what you type after /verity-prove. On security-sensitive code it models the attacker's side too: tenant isolation, revoked access, one-time tokens, event order, and check-then-use.
Only a reproduced bug blocks
A failure in the model is a fact about the model. It counts only when the same sequence, run on the real function in a container with no network, does what the model said. If the replay disagrees, the model was wrong and nothing happens.
Before a reproduced bug blocks, Verity follows the code to its entry point and looks for what would stop it in production: a lock, a unique constraint, a transaction. If something does, the finding shows as checked and the push goes through.
formal: runSeed in src/seed.ts · 2 rounds · 96 s · $0.31 the seed runs at most once REPRODUCED no partial seed holds high src/seed.ts:3 runSeed breaks "the seed runs at most once" Trace: runSeed → runSeed Replay: both calls passed the existsSync guard and posted 6 nodes # what most pushes print formal: skipped (no-candidate: no changed function scored above the bar)
Verity uses Lean to search for bugs, and makes no claim that your code is correct. A model that holds is not a pass for your code, and Verity never reports it as one.
Found in real code
We pointed the formal checks at 164 recently merged pull requests from 34 open-source projects. A separate AI review confirmed 7 bugs, and we found no earlier report of 5 of them. All 7 sat in older code next to the change, where a diff review does not look.
One was in Cal.com: a failed calendar answer read as a free slot, so a booking could land on top of an existing meeting. The code had been there since 2022. We reported it with two failing tests (calcom/cal.diy#30382), and contributors opened two fix PRs within two days.
On by default, and cheap to leave on
It runs on one function per push at most, and only when the push touches code worth modelling: money, auth, a transaction, a retry, a check followed by a write, or a file that history says has been fixed before. Most pushes stop in under a second and say why.
A push spends at most $1 and finishes inside the push review's three minutes. Each repository has a daily cap of five models and $5. New projects get it on, and Lean installs in the background. When you have a specific worry, ask for a check yourself with /verity-prove in Claude Code.
A failure can be replayed, and so can block a push, in TypeScript, JavaScript and Python. In other languages Verity stops before it writes a model. Lean takes about 2.7 GB of disk.
Agents write the code.
Verity keeps it true.
Start on the Free plan. Working with Claude Code today.
npm install -g @codacy/verity-cli && verity initWorks with