Apex∎

What it is

Apex is a formal verification framework for Python, written in Python, with Lean 4 as its proof engine. It reads what you have — prose specifications, docstrings, a test suite, the function body — unifies those into a single formal specification, generates Lean 4 theorem statements from it, and attempts to prove them automatically.

Where a proof succeeds, you have a mathematical guarantee that holds for every input, not a sample of them. Where a proof does not succeed, Apex produces a gap report: a specific, readable account of which obligation was not discharged and what would be needed to discharge it.

Both outcomes are the product. The framework is designed on the assumption that the second one happens more often, and that it is still worth having.

The problem it addresses

Code is now generated faster than it can be read. A model produces a function in two seconds; a careful review of that function takes minutes, and reviewers do not scale with generation. The usual answer is more tests, but tests are sampling. A test suite tells you the function behaved on the inputs someone thought to write down. It says nothing about the inputs nobody thought of — which, for machine-written code, are exactly the ones that matter, because the author had no intuition to encode in the first place.

Formal verification answers the universal question rather than the sampled one. Its historical problem is not power but access: writing Lean by hand requires a skill that most working engineers do not have and cannot justify acquiring for a single module.

Apex sits on that gap. The insight is that language models are unreliable at deciding whether something is true, but useful at proposing a formal statement of what someone meant. That proposal is then handed to a system that is very good at deciding truth and has no opinions at all.

Inputs, and why there are three

Most verification tools ask you to write a specification first. Apex assumes you already wrote one, three times over, in three incomplete forms:

English intent

Docstrings, comments, an issue description, a paragraph you type at the prompt. Rich in intent, weak in precision, and often the only place a precondition is ever recorded.

The test suite

Precise but partial. Each test is a concrete point on a curve nobody drew. Useful for pinning down edge-case intent and for catching a specification that contradicts observed behaviour.

The source

Total but silent about purpose. It says exactly what happens and nothing about what should. It also supplies the types, the control flow, and the definitions Lean will need.

Unification is where the interesting work happens. Three partial views of the same intent will disagree, and the disagreements are informative: a docstring that promises something the tests never check, a test that asserts behaviour the prose forbids. Apex surfaces those conflicts rather than silently picking one.

The pipeline

The trust model

The architecture draws one hard line. On one side sits every component that guesses: the model that reads your prose, the heuristics that reconcile a test suite with a docstring, the tactic search that hunts for a proof. On the other side sits the Lean 4 kernel, which does not guess.

Artifacts cross that line in one direction only, and they cross as candidates. A proposed proof term is either accepted by the kernel or it is not, and no amount of model confidence changes the answer. This means a hallucinated proof is not a silent failure — it is a rejected term, which is a normal, visible, reportable event.

Three outcomes, all of them useful

Each obligation Apex generates terminates in one of three states. A tool that only reports the first one would be nearly useless in practice, because on real code the first one is not the common case.

The gap report

When automation cannot discharge an obligation, the interesting question is why not, and there are only a few honest answers: a precondition was never stated, a supporting lemma is absent, the specification is stronger than the code, or the search simply ran out of budget. Apex distinguishes these and says which one it hit.

In practice the most valuable gaps are unstated preconditions. They are the assumptions a human author held in their head and never wrote down — and, for generated code, assumptions nobody ever held at all.

That last line is the point. Apex does not decide which fix is correct, because the two fixes mean different things to whoever uses the function. It makes the choice visible and forces it to be made deliberately.

A worked example

The input — an ordinary pure function with an ordinary docstring:

def clamp(x: float, lo: float, hi: float) -> float:
    """Constrain x to the range [lo, hi].

    Values below lo become lo; values above hi become hi;
    values already in range are returned unchanged.
    """
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

Two obligations fall out of that docstring. The first is a bounds claim, the second an identity claim — and the prose states both, in the two halves of its second sentence:

def clamp (x lo hi : ℝ) : ℝ :=
  if x < lo then lo else if x > hi then hi else x

theorem clamp_in_bounds (x lo hi : ℝ) (h : lo ≤ hi) :
    lo ≤ clamp x lo hi ∧ clamp x lo hi ≤ hi

theorem clamp_id_in_range (x lo hi : ℝ) (h₁ : lo ≤ x) (h₂ : x ≤ hi) :
    clamp x lo hi = x

The generated Lean 4 model and its two obligations. The hypothesis h : lo ≤ hi is the gap from §7, promoted into the statement.

The second theorem proves without difficulty. The first does not, until that hypothesis is added — and finding that hypothesis, rather than proving the theorem, is the work Apex actually saved.

Surfaces

Apex is delivered two ways, aimed at two different moments.

Command line

For running against a file or a package, in a terminal or in CI. The exit status distinguishes proved, gapped, and refuted, so a pipeline can decide what to do with each.

$ apex verify src/geometry.py --function clamp

  clamp_id_in_range      proved
  clamp_in_bounds        gap — unstated precondition (lo ≤ hi)

  1 proved, 1 gap, 0 refuted

MCP server

For the moment the code is written. Exposed over the Model Context Protocol, Apex becomes a tool a coding agent can call on its own output — so a model that has just generated a function can ask for a proof before proposing it, and receive a gap report it can act on. This is the closing of the loop the framework is named for: generation and verification in the same turn, with the verification half not trusting the generation half.

Scope

The MVP is deliberately narrow. Pure Python functions only — no side effects, no mutation, no I/O, no global state. This is not a limitation to be apologised for; it is the region where automatic translation to Lean is tractable and where the proofs mean something clean.

JavaScript support and editor integration are both deferred to post-talk phases. Widening the language surface before the core translation and reporting are trustworthy would produce a tool that is broad and useless.