formal

Lock the statement of a theorem a human approved, and see which proof files still have holes. For Lean 4 and Rocq. Every subcommand here runs offline.

The lock workflow

1. A human reads a theorem statement and decides it says the right thing.
2. Run paranoid formal lock <name>. It writes the statement hash to .paranoid-specs.json at the repo root.
3. Commit the lock file.
4. From then on, verify guards it. FV004 (critical) fires if a locked statement changes or its declaration disappears. FV007 (high) fires on any edit to the lock file. FV008 (medium) fires if the locked proof and the code it names change in the same diff.

An agent can run formal lock too. FV007 reports every change to the lock file so that a human can review it. See the FV rules.

A single critical finding, such as FV004 or FV006, gives a warn verdict, the same as in every other category. A warn already exits with code 1, so CI and the Stop hook block on it. If your repo relies on proofs, set strict = true in .paranoid.toml so any warn becomes a fail.

The spec lock file

.paranoid-specs.json sits at the repo root. FV004 compares the head against the lock as it was at base, so editing the lock in the same diff does not hide a change.

{
  "version": 1,
  "specs": [
    {
      "name": "Parser.parse_total",
      "file": "Proofs/Parser.lean",
      "statement_sha256": "<64 lowercase hex characters>",
      "code": "internal/parser/parse.go",
      "note": "parse never fails on valid UTF-8"
    }
  ]
}

version must be 1. name, file, and statement_sha256 are required. code and note are optional; code turns on FV008 for that spec. The hash is the SHA-256 of the normalized statement (comments removed, runs of whitespace collapsed to one space), written as lowercase hex. Specs are kept sorted by name, then file. A lock file that does not parse at base is reported as a skipped check named formal-verification/spec-lock. The commands below treat a lock file that does not parse as an error.

paranoid formal lock

paranoid formal lock <name>... [--file path] [--code path] [--note text]

Run it inside the repository. It reads the tracked .lean and .v files in the working tree, finds each declaration by its exact qualified name (for example MyList.rev_rev), hashes its statement, and adds or updates its entry in .paranoid-specs.json. It creates the file if it is missing and keeps other entries. It prints one line per name:

locked MyList.rev_rev (Proofs/Rev.lean) sha256:abcd12345678...

--code and --note apply to every name given. When you update an existing entry, its old code and note are kept unless you pass the flag again. If a name is defined in more than one file and you gave no --file, the command fails and lists the files. If a name is not found, it fails and suggests paranoid formal status. Nothing is written when any name fails.

paranoid formal unlock

paranoid formal unlock <name>...

Removes the entries with these names from the lock file. It fails with an error, and writes nothing, if a name is not locked.

paranoid formal status

paranoid formal status

Prints a plain text report in a fixed order. It has two sections.

• Locked specs. Each spec is ok, drifted (the statement hash differs from the lock), or missing (the declaration or its file is gone).
• Proof files. Each tracked .lean or .v file that has holes or axioms and escapes, with counts, for example Proofs/Rev.lean: 1 hole, 1 axiom or escape. none when all are clean.

A last line gives the totals. Only tracked files are read, and each is read once.

paranoid verify shows the same numbers, taken at head, in its Proofs block.

Demo

hack/demo/formal.sh builds a throwaway Lean project with one honest theorem and one locked spec. It then acts as an agent that cheats: it adds sorry and an axiom, weakens the locked theorem, and turns on a soundness switch. It runs paranoid formal status and paranoid verify so you see FV001, FV002, FV004, FV006, and the Proofs block. It needs no Lean install, no container, and no network, and it deletes its temp directory when it ends. From the repository root:

sh hack/demo/formal.sh

Exit codes

Exit 2 is the same "check failed" code that verify uses. Holes and escapes alone do not change the status exit code; verify reports those as FV001 and FV002. See Exit codes & CI.

Clean-room re-check (opt-in)

paranoid verify --formal-check

The rules above read text. --formal-check asks the proof checker instead. It rebuilds the proof project in a container, then asks the kernel which axioms each audited theorem depends on. A sorry hidden behind a macro or a notation still shows up as sorryAx. Without the flag nothing changes in any report.

It uses the runtime chosen by --sandbox (docker or podman). With --sandbox none the re-check is listed as skipped, with no finding. See Sandbox & coverage for how the containers run.

Which project is rebuilt

A project at the repo root is found first. If the root has none, a Lean project in the formal/ folder is found (the folder formal prove creates). A Rocq project is found only at the root.

• Lean: lean-toolchain plus lakefile.lean or lakefile.toml, at the root or in formal/. For formal/ the container builds from that folder. Image debian:bookworm-slim. With the network on, the prep step installs the toolchain named in lean-toolchain and fetches the Lake dependencies. For Mathlib it also runs lake exe cache get. With the network off, the check step runs lake build, then #print axioms on a generated file.
• Rocq: _CoqProject, or a dune-project with a Coq or Rocq stanza. Image rocq/rocq-prover:9.1. With the network off, the check step builds with dune build when there is a dune-project, otherwise from a makefile generated from _CoqProject. Then it runs Print Assumptions on a generated file. Both the rocq command and the older coq_makefile and coqc are handled.

Which theorems are audited

Every spec in the head lock file, plus every theorem declared in a changed proof file of the project's language, sorted by file and name, at most 200. Lean private declarations are left out, because they cannot be named from another file; any axiom they use also shows up in every public theorem that uses them. Rocq theorems in a Module are printed with their full path. A theorem the checker cannot find by name (for example a name made by a macro) is reported as FV012, not skipped.

Allowed axioms

Lean allows propext, Classical.choice, and Quot.sound. Rocq allows none. A .paranoid.toml list adds to that set:

[formal]
allowed_axioms = ["Classical.choice"]

sorryAx, Lean.ofReduceBool, and Lean.trustCompiler are never allowed. Listing one is a policy error (exit 3). See Team policy file. A Rocq theorem that ends in Admitted. shows up as an axiom named after the theorem, so FV010 fires on it.

The rules

When the re-check runs, the report lists the check formal-verification/recheck in checks_run. When it cannot run, the same name is in checks_skipped with the reason, and FV011 carries the reason as evidence.

What this does and does not prove

• The rules read text. An agent can hide a hole behind a macro or a notation. The opt-in re-check asks the checker itself, which covers this case.
• A proof is about a theorem. paranoid can show the theorem did not change since a human approved it. It cannot tell you the approved theorem says what you meant.
• Proofs made for code in other languages are about a Lean model of that code. Tests that compare the model and the code can show they agree on many inputs, not on all inputs.

Online features and providers

Some paranoid formal subcommands call an LLM. fill and prove are in this build (see below). Both use the same provider clients, settings, caps, and request log.

paranoid formal providers

paranoid formal providers [--task proof|spec] [--provider P] [--model M] [--base-url URL]

Shows what an online command would use, with no network call. For each task (both, or the one in --task) it prints the provider, model, base URL, and the environment variable the key is read from, with (set) or (not set). The key itself, or any part of it, is never printed.

task: proof
  provider: openai
  model:    my-local-prover
  base url: http://localhost:11434/v1
  key from: LOCAL_LLM_KEY (set)

Exit 0, or 3 on a configuration error (for example a secret in the policy file, or no model for a provider that has no default).

paranoid formal fill

paranoid formal fill [path or name...] [--attempts N] [--dry-run] [--provider P] [--model M] [--base-url URL]
                     [--max-requests N] [--max-tokens N] [--timeout D] [--check-timeout D]

Fills proof holes (sorry, admit, Admitted) in the Lean or Rocq project at the repo root, or the Lean project in formal/. With no arguments it tries every hole in the tracked proof files of that language. An argument that ends in .lean or .v is a file (all its holes). Any other argument is the qualified name of one theorem or lemma. It uses the proof task settings.

What is sent

Before the first call the command prints the provider, the model, and the files whose content will be sent. For each hole the model gets the whole file, the declaration, and on a retry the latest checker output and its own last answer. It is told to answer with one fenced code block holding only the replacement proof (Lean: the term or by block after :=; Rocq: Proof. through Qed.), never to change the statement, and never to use holes, axioms, or escape hatches. Any other shape of answer is rejected.

The gate

An answer is accepted only when all of these hold. It is spliced into a scratch copy, and only the proof span changes.

• The local checker exits 0 (Lean: lake env lean from the project folder; Rocq: rocq compile or coqc with the -Q and -R flags of _CoqProject).
• A re-parse shows the same declarations, the same statement hash for the target, and unchanged text for every other declaration. No extra command follows the proof, and the new proof has no hole or escape.
• The static rules FV001, FV002, and FV006 find nothing new, comparing the original file with the candidate.
• A kernel axiom audit of the target, run in the scratch copy, gives an answer and lists only allowed axioms (the same set as the re-check, including the policy [formal] allowed_axioms list; sorryAx is never allowed).

Output and exit codes

Accepted proofs are written to the worktree, or shown as a diff with --dry-run. Each declaration ends as filled, failed (with the first lines of the last checker error), or skipped (a cap or the run timeout was hit, and the line names it). Exit 0 when every hole was filled, 2 otherwise, 3 on an error (no key, a provider error, no proof project, toolchain not found).

Needs a local toolchain. In this version the checker runs on your machine, so Lean (lake) or Rocq must be installed. If it is not, the command stops with a message. paranoid verify --formal-check stays the final word: it rebuilds the project in a clean container.

paranoid formal prove

paranoid formal prove <file>:<symbol>... [--continue] [--attempts N] [--cases N] [--seed N]
                     [--lean-toolchain T] [--force] [--provider P] [--model M] [--base-url URL]
                     [--max-requests N] [--max-tokens N] [--timeout D]

Builds a proof about a function in Go, Python, or TypeScript. It works in two steps with a person in between. Each hotspot is <file>:<symbol>; the rules for what a hotspot can be are below. An unsupported hotspot is printed as refused with the reason, and the run ends with exit 3 once the others are done.

Step 1: draft (the default)

1. Extract. Each hotspot is read and its span is printed (path, line range, and the signature) so you can check the boundaries.
2. Lake project. The Lean project at the repo root is used if there is one. Otherwise formal/ is created with lakefile.toml (a lean_lib named Formal), lean-toolchain, and a .gitignore for .lake/. The toolchain is --lean-toolchain, else the repo's own lean-toolchain, else leanprover/lean4:v4.24.0. A project that exists is never rewritten. A root project must have a library named Formal. The models use the Int8 to Int64 and UInt8 to UInt64 types, which need a recent Lean.
3. Ask. The spec provider is asked for one fenced Lean block: namespace Paranoid.<File><Symbol>, a def model with exactly the signature paranoid derives, and two to five theorems about model. Each theorem has a doc comment with one plain-English sentence and a proof of exactly by sorry. The prompt explains the type rules (fixed-width integers wrap like the source language, Python integers do not, how division and strings behave) and forbids axioms and escape hatches.
4. Validate. The block is checked before anything is built. It must parse. The model signature must match after whitespace is normalized. The model and any helper before the first theorem must have no hole. Every theorem must mention model. The rule marks FV002 (axioms and escapes) and FV006 (checker switches) must find nothing, and so must a short list of other commands (macros, notation, set_option, attributes, # commands, partial, opaque). Nothing may sit outside the namespace except import lines. A rejected answer is sent back with the reason.
5. Write. The file goes to Formal/Paranoid/<File><Symbol>.lean under the Lake root. An existing file is not overwritten unless you pass --force.
6. Build and compare. lake build builds the module (the sorry warnings are fine). Then the differential test runs. On a build error, or a mismatch, the errors or the first differing inputs go back to the model for another draft, up to --attempts. The model must match the code before you review anything. If no draft matches, the file is removed and nothing is kept.
7. Print. The candidate specs are printed with the theorem name, its English line, and its Lean statement, then the exact next steps: read the file, git add it, run paranoid formal lock <names> --code <hotspot file>, then paranoid formal prove --continue <file>:<symbol>. (lock and fill read tracked files, so the model file must be added first.)

The draft step proves nothing. It checks that the model agrees with the code on the generated inputs, and gives you statements to read.

Step 2: --continue

1. Find the locked specs. Only specs whose file is the hotspot's model file and whose code is the hotspot's source file count. With none, the command refuses (exit 3): a person has to approve first. An unlocked theorem is never sent to the model. If a locked statement changed since it was locked, or the model file no longer has the required signature, the command stops with exit 3 before any call.
2. Fill. The same loop and the same gate as formal fill (task proof), on the locked theorems that still have a hole.
3. Audit. The kernel axiom audit is run on every locked theorem in the final file, including ones that already had a proof. Each must give an answer with allowed axioms only.
4. Rebuild and compare. The module is rebuilt and the differential test runs again. The model must still match the code.

The last line is one of these:

Proved on the Lean model. The model matches the code on N generated inputs.

It is printed only when every locked theorem was filled or already proved and passed the audit, the model builds, and the differential test passed. Otherwise the last line starts with Not proved. and says what is missing: which theorems are not proved, or how many inputs differ. The output never says the code is proven.

What is sent

Before the first call the command prints the provider, the model, and what will be sent. The draft step sends, for each hotspot, the function source (the extracted span only, not the file), its language, and the required Lean signature. On a retry it also sends the model's own last answer and the build errors or the first differing inputs. No other file is sent. The --continue step sends the whole model file, once for each theorem it tries, plus the latest checker output on a retry. Every call goes through the same logged client as fill, so the request log shows exactly what left your machine.

Exit codes

Needs a local toolchain. Like fill, the checker runs on your machine, so lake must be installed, and so must go, python3, or node for the language of the hotspot. Only those four programs are run, each with a timeout. If the project's Lean toolchain is not installed, elan may download it the first time lake runs. paranoid itself makes no network call except the provider calls.

What this proves. A finished run proves the locked theorems about the Lean model, and shows the model and the code agree on the generated inputs. It does not prove the code correct, and it does not prove the theorems say what you meant. That is why a person reads and locks them first.

Providers

The clients use net/http only. There are no provider SDKs.

Keys and settings

• Keys come from environment variables only. There is no key field in any file. A .paranoid.toml entry may name a different variable with api_key_env, never the key itself. A field that looks like a secret (api_key, key, token, secret) is a policy error.
• No fallback. If the key variable is empty, the command stops and names the variable to set. It never tries another provider.
• Per task. The tasks are proof (proof search) and spec (spec drafting and Lean models). Each can use its own provider. A task falls back to [formal.llm], field by field. A table that names a different provider than the one in use does not lend its model, base URL, or key variable.
• Flags override files. --provider, --model, and --base-url override the file. Precedence per field: flag, task table, [formal.llm], default.

The fields are documented on the policy page.

What gets sent

Only what the command needs for the task: the proof or spec text, the declaration, and the latest checker errors. Before the first call, the command prints the provider, the model, and which files' content will be sent. Nothing is sent from the offline commands.

Caps

Every online run has caps, on by default. The run stops at a cap and the error names it.

Retries happen only on HTTP 429 and 5xx answers and on a connection that drops before the reply is complete, at most 3 times, waiting for the provider's retry-after when it sends one. Other errors, such as a refused key, stop at once.

The request log

Each online run writes .paranoid/formal/runs/<run-id>.jsonl. The run id is the UTC start time, like 20260102T030405Z (with -2, -3 if two runs start in the same second). One line per call, with: sequence number, time, provider, model, input and output token counts, stop reason, the system prompt, the messages, the max tokens, the full response text, and an error text when the call failed. You can read exactly what left your machine. API keys and auth headers are never written. The file is private (mode 0600). It holds your code, so do not commit it.

Proofs and the code they describe

This is the contract paranoid formal prove follows: what a hotspot can be, how the model is compared with your code, and what the report may claim.

A paranoid-made proof is about a Lean model of your function, not about the function. To connect the two, paranoid runs your real function and the Lean model on the same generated inputs and compares the answers.

What a hotspot can be

A hotspot is <file>:<symbol>. v1 takes only a top-level, pure, total function with one return value, on integers, booleans, strings, and lists of those (lists may nest). Anything else is refused with a reason. Go (a (T, error) return is refused), Python (type hints on every parameter and the return), and TS (annotations required, .ts only, Node 22.6 or newer) are supported. Plain .js is refused.

The Lean model must have the exact signature paranoid derives, for example def model (xs : Array Int64) (k : Int64) : Int64, inside the namespace Paranoid.<File><Symbol>.

The differential test

• paranoid writes the harnesses, not the LLM. Both are written from fixed templates and the function signature. For Go, a temporary test file runs in a temp copy of the repo, so unexported functions work. Python runs under python3 -I. TS runs under node --experimental-strip-types. Lean runs lake env lean --run on a generated main. The model can not change how it is called.
• Inputs. A seeded generator with a fixed default seed, so the same seed gives the same inputs byte for byte. Edge values come first (0, 1, -1, the minimum and maximum of the type, empty string, "é", Japanese text, an emoji, empty list, one-element list). Then random values. The default is 1,000 inputs.
• Compare. The outputs are compared as canonical JSON, one input at a time. A panic or exception in the real function counts as a failure and names the input. v1 supports total functions only.
• Programs run. Only go, python3, node, and lake, each with a timeout. Your tree is copied first and never changed.

The trust statement

On success the last line of formal prove --continue says: Proved on the Lean model. The model matches the code on N generated inputs. It never says the code is proven. Matching on N inputs is evidence that depends on the generated inputs. It is not a proof.