Proven

Proven

A judge for code written by AI. The syntax is plain Python. The rules are against hallucinations.

The core principle: nothing exists until it is proven. A package exists if it is pinned in requirements. A function exists if it is in the installed version. A fact exists if it has a source and a date. A model's answer exists for the user once it has passed a check. A function works if a test proves it.

Why

AI models write more code than people can read. The languages that win are the ones where the compiler acts as a reviewer: TypeScript became the #1 language on GitHub in 2025 (GitHub Octoverse 2025), and GitHub links this to typed languages making AI-assisted code more reliable. A new language is not the answer — models barely know new languages. What helps is the old language that models know best, with a strict judge on top of it. That is how TypeScript grew on top of JavaScript.

Proven does the same for Python, but it catches hallucinations rather than type errors.

Six rules

Every rule in detail: SPEC.md.

What it looks like

The code in examples/bad/bot.py is how an AI model writes when nobody checks it — a legal-answers bot for Kazakhstan:

import anthropik                     # a typo

MRP = 3932 # Kazakhstan's monthly index, the 2025 value "from memory"

def handle(phone, question): raw = llm(question) answer = f"{raw}\n\nLegal basis: Article 46 of the Labour Code" try: json.loadz(answer) except: pass send(phone, answer)

The judge:

$ python proven.py check examples/bad

Proven 0.2.0 · root: /path/to/proven/examples · python: /usr/bin/python3 3.12.3 · requirements: requirements.txt · packages from: the judge's own

bad/bot.py:4:1 P1 package "anthropik" is not in requirements.txt — it may be invented bad/bot.py:5:1 P1 version of "requests" is not pinned with == (now: ">=2.31") bad/bot.py:7:1 P3 "MRP" is a number typed from memory — it needs a dated source bad/bot.py:9:10 P3 address "adilet.zan.kz" typed by hand — move it to a config or allowed_url_hosts bad/bot.py:12:1 P6 function "llm" is not called in any test bad/bot.py:16:5 P4 public function "llm" returns unverified model output — annotate it "-> Unverified" or return verify(...) bad/bot.py:19:1 P6 function "send" is not called in any test bad/bot.py:23:1 P6 function "handle" is not called in any test bad/bot.py:25:14 P3 law article number typed by hand: "Article 46" — take it from the database bad/bot.py:27:9 P2 module "json" has no name "loadz" bad/bot.py:28:5 P5 bare except catches everything, even Ctrl+C and program exit bad/bot.py:30:5 P4 unverified model output goes into "send"

How to fix: P1 Imports are real — Check the exact package name on PyPI, add a name==version line ... ...

Proven: 12 issue(s) in 1 file(s). Code rejected.

The same bot fixed according to the rules — examples/good/bot.py:

MRP = Fact(4325, source='Law of the Republic of Kazakhstan "On the Republican Budget '

'for 2026–2028" No. 239-VIII', date="2026-01-01")

def ask_model(question, llm) -> Unverified: return unverified(llm(question))

def answer(question, llm, checker, send): raw = ask_model(question, llm) send(verify(raw, checker)) # the user only gets what has been verified

$ python proven.py check examples/good Proven: no issues. Code accepted.

Quick start

Python 3.11+. No dependencies — the standard library only.

pip install proven-judge        # the package is "proven-judge", the command is "proven"

proven init # create proven.toml proven check # check the project

Exit code: 0 — code accepted, 1 — there are issues. For machines there is --json.

proven rules                    # list the rules

proven explain P4 # explain a rule

In your code, from proven_types import Fact, Unverified, unverified, verify, and add proven-judge==0.2.0 to requirements.txt (P1 applies to Proven too).

No installation at all: copy proven.py and proven_types.py into your project and run python proven.py check.

pre-commit

# .pre-commit-config.yaml

repos:

• repo: https://github.com/malikabyl/proven rev: v0.2.0 hooks:
• id: proven

The hook checks the whole project, not only the changed files: P6 needs to see the tests.

GitHub Actions

- uses: actions/checkout@v4

• uses: malikabyl/proven@v0.2.0

Issues show up as annotations on the lines of the pull request and in the job summary. Inputs: path (the folder to run in), args (extra arguments for proven check), python (the interpreter with your dependencies installed, so P1 and P2 can see them; by default python3). Outside the action, proven check --github gives the same annotations.

MCP server

Proven is also an MCP server, so an AI agent can call the judge itself: tools proven_check, proven_explain and proven_rules. It needs no extra packages.

Claude Code:

claude mcp add proven -- uvx proven-judge mcp --no-installed-check

Other clients (Claude Desktop, Cursor and others):

{

"mcpServers": { "proven": { "command": "uvx", "args": ["proven-judge", "mcp", "--no-installed-check"] } } }

uvx runs the server in its own environment, where your project's packages are not installed, hence --no-installed-check. To check that packages are installed too (P1), run the server from your project's environment instead: pip install proven-judge, then proven mcp. Pass the agent an absolute path to the project.

The loop with an AI model

Proven works like a compiler for an AI model: the model writes code, the judge says what is wrong and how to fix it, the model fixes it. The judge's messages are written so they can be handed to a model as they are.

Claude Code. The repository already has .claude/settings.json: after every edit of a .py file the judge checks it, and if there are issues, Claude sees the report and fixes them. Copy the .claude folder into your project.

Rules in the prompt. A cheat sheet for a system prompt or CLAUDE.md is in PROMPT.md. The model then follows the rules from the first try, and the judge catches the rest.

GitHub. The workflow .github/workflows/proven.yml runs the judge and the tests on every push and pull request.

An existing project

On old code the judge will find many issues at once. To avoid fixing everything in one day:

python proven.py baseline

The current issues are written to .proven-baseline.json as old debt. From then on the judge skips them but rejects any new issue. Pay the debt off gradually and rewrite the baseline.

Run the judge with the project's Python. P1 and P2 look at installed packages. The first line of every report says what the judge measured with: the project root, the Python, the requirements file and the environments it read. Without proven.toml the root is the nearest folder with pyproject.toml, requirements.txt or .git. If the judge runs in its own environment, it also reads the project's .venv (or venv, env, $VIRTUAL_ENV): packages there count as installed, and names in them are checked by reading their code, without importing it.

A project with no tests at all gets one P6 issue instead of one per function. Until there are tests, disable = ["P6"] keeps the report readable.

Waivers

The human has the final say. A rule can be switched off for one line — but only with a reason:

MRP = 3932  # proven: allow P3: computing an archived 2025 fine

A waiver without a reason is itself an issue (P0). The comment goes on the same line or on the line above. For P5 it can also go inside the handler, where the explanation usually is:

except OSError:

pass # proven: allow P5: logging a call must not break the answer to the client

A plain comment is not enough on purpose: a model can write "# intentional" as easily as "pass". The Russian keyword works too: # proven: разрешить P3: reason.

Honest limits

The judge catches what is invented, not what is wrong:

• P3 checks that a fact has a source and a recent date, not that the value matches the law. Comparing it with the source is up to a person or to the check in verify().
• P2 checks names in modules and classes. Methods on objects (response.jsonn()) cannot be checked statically — tests catch them (P6).
• P2 imports packages installed in the judge's own environment to look inside, which runs their import code; packages from the project's .venv are read, not imported. Turn it off with check_attributes = false.
• P4 follows data inside a file and through functions by name. It is cautious: when in doubt, it treats data as unverified. A public function that returns model output must say so with -> Unverified. A model client created in another file is only recognised if its function name is listed in sources.
• P6 matches functions and tests by name, not by module.
• Logic that is wrong but consistent will not be caught by any static judge. Tests and your final word catch it.

Layout

proven.py             the judge (CLI)

proven_types.py Unverified, Verified, verify(), Fact proven.toml settings (the judge checks itself) SPEC.md the rules in detail and every setting CHANGELOG.md what changed in each version PROMPT.md a cheat sheet for an AI model examples/bad code with hallucinations examples/good the same code following the rules tests/ the judge's tests pyproject.toml the proven-judge package action.yml the GitHub Action server.json the MCP Registry entry .pre-commit-hooks.yaml the pre-commit hook .claude/settings.json the hook for Claude Code .github/workflows/ the check on GitHub and the release to PyPI

Releasing: bump VERSION in proven.py, then publish a GitHub release with the tag vX.Y.Z. The release workflow checks that the tag, VERSION and server.json agree, builds the package, publishes it to PyPI and then to the MCP Registry. Update the two versions in server.json together with VERSION.

Check the judge itself:

pip install -r requirements-dev.txt

python proven.py check # the judge accepts itself python -m pytest

The values in the examples (Kazakhstan's MRP and others) were checked against the source on 3 November 2026 and serve as illustrations. In live code, check them against adilet.zan.kz, Kazakhstan's official legal database.

License

MIT, see LICENSE.