git:20260618.54db1ba to git:20260702.917841b

---

description: The Method — close an OPEN Aver proof law by having an agent propose auxiliary helper lemmas, test them with `aver proof --discover`/`--check`, and refine until the Lean kernel / Z3 certifies the law. Works on any Aver project; the agent proposes, the judge decides.

allowed-tools: Bash, Read, Write, Workflow

---

# The Method

A reusable loop for closing an OPEN Aver `verify ... law` in **any** Aver project. An agent

PROPOSES auxiliary helper lemmas, `aver` TESTS them, and the Lean kernel / Z3 JUDGES whether the

target law now closes — looping until it closes or a budget runs out. The LLM proposer is the only

unbounded source of new lemmas; the judge keeps it sound.

## When to use

- A `verify ... law` is open in Lean (often already provable by Z3/Dafny — then this kernel-

certifies it in Lean).

- A goal that needs an auxiliary lemma the auto-prover can't find on its own (a missing

homomorphism / associativity / distributivity / an equation relating subterms of the goal).

## Usage

```

/the-method <task.av> [<task2.av> ...]

```

Run from your Aver project root. Paths are relative to that root, or absolute. The loop auto-detects

the `aver` binary (`./target/release/aver`, `./target/debug/aver`, or `aver` on PATH; it will build

it if missing). You can also invoke the engine directly:

```

Workflow({ scriptPath: "<this-skill-dir>/the-method-loop.js", args: { tasks: ["path/to/task.av"], attempts: 4 } })

```

## How it runs

The conjecturer and the prover are SEPARATE, capability-fenced agents — "the agent proposes, the

kernel decides" is enforced structurally, not merely asked. One independent chain per task, run in

parallel; within a chain, up to `attempts` propose→test rounds:

1. **Conjecturer** (`the-method-proposer`, **Read+Glob only** — no toolchain, no Bash, cannot open

any generated `.lean`/`.dfy`): reads the target (and one `decomposed/` example, if present) and

proposes 1–3 true, general helper laws aimed at the open goal — never a restatement.

2. **Runner** (`the-method-runner`): mechanically splices the laws into a `/tmp` copy — **before**

the target `verify ... law` (order + rendering matter) — then runs a **three-stage sieve**,

cheapest first: (a) `aver check` (parse/typecheck — a malformed law caught + fed straight back);

(b) **`aver verify`** (bounded sample eval, no Lean — an INDEPENDENT Aver-semantics check: a law

FALSE on its samples, e.g. a `Nat`-returning fn bridged to an `Int`-returning builtin, is

rejected here as `false-on-samples`, before any Lean — this catches the class the kernel proof

can wrongly accept because its own bounded check shares the Lean translation); (c) only if verify

is clean, `aver proof --check --check-json --backend lean`. A closure requires **both**

`verifyClean` AND `universal:true`/`sorries:0`. The runner returns **only the Aver-level verdict**

(per-law `lawStatus`: proven / sample-only / open / false-on-samples) — the Lean residual never

crosses back. **No `--discover`**: The Method measures the LLM-proposed laws + our auto-prover,

not the enumerative recognizer; a closure is self-contained, and the conjecturer must supply every

law (including bridges to builtins like `List.concat`/`List.reverse`).

3. On failure the conjecturer refines against that Aver-level verdict; on `"universal":true` with

`"sorries":0` the chain closes.

Because the conjecturer physically cannot see the proof, it cannot drift from conjecturing into

tactic/prover-internals debugging (the measured dominant cost sink). The `model` override sets the

conjecturer; the runner and verify gate stay on the session model by default. (The runner is

mechanical but must read the verdict ACCURATELY — the loop only verifies a self-reported close, so a

runner that under-reports silently drops a real win; a measured run showed a `haiku` runner doing

exactly that, for marginal cost saving. Pass `runnerModel`/`verifierModel` to override, accepting

that risk.)

Then a **Verify** phase (`the-method-verifier`) independently re-checks each claimed closure from

scratch (a fresh dir) — a self-reported closure is not trusted on its own — and persists the

verified decomposition to `decomposed/`. Only verified closures are returned.

## Output

Per task: `closed`, `verified`, `attempts`, `helperLaws` ({name, source}), `summary`; plus a

`verifiedClosed` count and a `winners` list ([{task, helperLaws}]) ready to save as `decomposed/`

entries.

## Do no harm

Keep a proposed lemma set only if the augmented task still closes — never let a committed lemma

regress a proof that worked without it.

## Safety

The conjecturer and runner are READ-ONLY on the project — all proof work happens on `/tmp` scratch

copies. The ONLY sanctioned project-file write is the verify gate persisting a re-confirmed win to

`decomposed/`. The loop never runs state-changing `git` commands and never modifies your source.