AI code review guesses.
It reads the code and gives an opinion. Generated code usually looks right, so an off-by-one slips straight through.
Your agent says it works. Apex proves it.
Apex Verify checks every function your coding agent writes against your docs, specs and tests. You get a machine-checked proof, or the exact input that breaks it. Never a guess.
AI review guesses. Tests sample. Apex proves.
Agents write code faster than anyone can read it. The usual checks weren’t built for that.
Tests sample.
They check the inputs someone thought of. Bugs live at the others: an empty list, a negative number, a boundary.
Your agent grades itself.
When the same model writes the code and the tests, they share the same mistake. “It works” is just more generated text.
Three verification engines. You don’t need to know any of them.
Apex reads the intent you’ve already written, turns it into formal statements, and sends each function to the engines that fit. Every failure is replayed on your real code before you see it, and every result says how strong it is: proof, evidence, or a failure you can reproduce.
What you already have
CodePython, JavaScript, TypeScript
IntentDocstrings, specs, tests
ApexTurns your intent into formal statements and routes each function
Lean 4Proves it for every input
FuzzingHunts for a failing input in your real code
TLA+Checks every thread interleaving
One reportA proof, or the input that breaks it
TerminalCoding agentCI
Runs where your agent already works.
One command adds the Apex skill and MCP server to your coding agent. Then ask it, in your own words, to verify a function. It runs Apex, reads each counterexample and fixes the code until it passes.
Terminal
apex skill install --with-mcp
- Claude Code
- Codex
- Gemini CLI
- Cursor
- VS Code (Copilot)
Built so that AI can’t fake a result.
The work is split into three roles, and no single role controls the verdict.
Propose
AI model or agentUntrusted
Statements, specs
Approve
Person at a terminalHuman
Approval
Decide
Lean 4 kernelTLCYour real code
Verdict
The model never has a direct path to the verdict.
Questions developers ask first.
No. Apex writes the theorems, specifications and campaigns, and runs the engines. You read each statement in plain English and in Lean before you approve it.
No. Apex reads the docstrings, JSDoc, tests and English spec files you already have. A short formal hint in backticks makes an English requirement checkable, and an AI model can write the hint for you.
A model can only propose. Lean compiles every proof cold and audits its axioms, and proofs that use sorry, native_decide, a user axiom or forged output are rejected. The release eval requires zero false proofs.
Proofs cover a subset of code: strings, floats, dicts, classes, while loops, recursion and exceptions go to fuzzing, which is evidence, not proof. TLA+ checks are bounded and cover invariants only, and there are no performance checks. A proof is also only as good as the statement you approve, so read it before you sign off.
No. Without a model, every deterministic step runs: tactic proofs, refutation, fuzzing and model checking. A model makes more proofs succeed and can draft hints and TLA+ specs.
Yes. apex check writes SARIF, so results show up as GitHub code-scanning alerts. Commit your approvals in .apex/reviews.json and CI reproduces the same proofs without a person.
Apex is free and MIT-licensed. Without a model it uses no paid service. The Lean toolchain and Mathlib cache take several gigabytes of disk, shared by all your projects.
Get started.
You need Python 3.12+ and uv. Add Java 11+ for TLA+ and Node.js 22.6+ for JavaScript and TypeScript.
Terminal
git clone https://github.com/hyperionaidev/apex && cd apex uv build && uv tool install dist/apex_verify-*.whl apex init # one-time: Lean toolchain and Mathlib cache apex doctor # checks the installation apex skill install --with-mcp # optional: add Apex to your coding agent
Apex isn’t on PyPI yet, so you build it from source. The first apex init downloads several gigabytes, once, shared by all your projects.