Kimi Code

ID kimi · Company Moonshot AI

Use Moonshot AI’s Kimi Code CLI as an automated theorem prover with Lean skills and MCP tooling. This prover uses the AgentProver with the KimiHarness.

Authentication

Kimi Code is included with every paid Kimi Code plan. Choose a plan and sign up if you don’t already have an account. Install the Kimi Code CLI and generate an ephemeral API token once on the host:

kimi login

Check you are properly authenticated with:

open-atp auth-status kimi

This writes OAuth credentials to ~/.kimi-code. By default the harness reads that file; pass it explicitly to override:

from pathlib import Path

from open_atp.harness import KimiHarness

KimiHarness(home_dir=Path("~/.kimi-code").expanduser())

The harness mounts the credential into the sandbox at run time so Kimi Code can refresh its access token mid-session, billing against your Kimi Code subscription. See Tracking cost and usage for details.

Warning

Token expiration: The token in ~/.kimi-code/credentials/kimi-code.json is valid for only about 15 minutes and it only renews when the Kimi CLI runs on the host. A sandboxed run will fail if the token expires mid-run. Check the time remaining with open-atp auth-status, and run kimi login on the host immediately before each run.

Using the prover

Standard prover via Python API

The simplest way to run the prover is through standard_prover() which uses a standard configuration. Here, we prove the MUL_REORDER example theorem:

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.config import standard_prover
from open_atp.examples import EXAMPLE, example_task

task = example_task(EXAMPLE.MUL_REORDER)
prover = standard_prover("kimi", backend=DockerBackend())
result = prover.prove(task, output_dir=Path("demo"))

Standard prover via CLI

The standard prover can also be run from the CLI:

open-atp prove path/to/task.lean output_dir kimi

Customizing the prover

To override knobs like model, construct the class directly:

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.examples import EXAMPLE, example_task
from open_atp.harness import KimiHarness
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers import AgentProver

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=KimiHarness(model="kimi-code/kimi-for-coding"),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all KimiHarness configuration options.

Harness details

By default, the Kimi Code harness is equipped with:

  • Official Lean skills [8].

  • lean-lsp-mcp MCP server [2].

The agent prompt (below) is written into the working directory and read into $PROMPT. The Kimi CLI is then invoked in non-interactive mode with $PROMPT as the input. See the script below for the full Kimi CLI invocation.

Agent Prompt
The working directory is a complete Lean 4 lake project. One or more `.lean`
files contain `sorry` (or `admit`) placeholders standing in for proofs that have
not been written yet. Replace every such placeholder with a real proof so the
project compiles cleanly and depends on no axioms beyond Lean's standard set.

Hard rules:
- Do not weaken, rename, restate, or delete any theorem, lemma, `def`,
  `structure`, or signature. Only fill in proof bodies (the part after `:=` /
  `by` that is currently `sorry`). Changing a statement to make it easier to
  prove is failure, not success.
- No new axioms and no `sorry`/`admit`/`native_decide`-on-false escapes. The
  finished proof must type-check honestly. The only acceptable axioms are Lean's
  standard `propext`, `Classical.choice`, and `Quot.sound`.
- Stay inside this working directory; do not read or write files outside it.
- Do not edit `lakefile.toml`/`lakefile.lean`, `lean-toolchain`, or
  `lake-manifest.json` — they pin the toolchain and dependencies and must match
  the verification environment.

Workflow:
1. Find the work: search for `sorry` across the `.lean` source files (e.g.
   `rg -n '\\bsorry\\b'`). Read each file containing one to understand the
   statement, the hypotheses, and the relevant imports.
2. Confirm the lean-lsp MCP server is live before relying on it: call
   `mcp__lean-lsp__lean_diagnostic_messages` on a file you have not yet edited.
   `success:true, items:[]` means it compiles cleanly; real errors come back as
   `items`. `success:false, items:[]` usually means the import oleans aren't
   materialized yet — run `lake env lean <file>` once to build them.
3. Write a proof for one `sorry` at a time. Mathlib is available; prefer library
   lemmas, `simp`, `omega`, `linarith`, `exact?`/`apply?` suggestions, and
   `aesop` over long bespoke arguments.
4. After each edit, re-check that file with
   `mcp__lean-lsp__lean_diagnostic_messages` and iterate until it is clean.
5. When a file looks done, verify it has no stubbed proofs with
   `mcp__lean-lsp__lean_verify` — the reported axioms must NOT contain `sorryAx`.
6. Repeat until no `.lean` file contains a `sorry` and every file compiles
   cleanly. Do the final compile check per file with `lake env lean <file>`:
   exit code 0 and no output means it compiles. This is the exact command the
   grader uses, so it is the source of truth.

Tips:
- Use the lean-lsp tools (`mcp__lean-lsp__*`) as your primary feedback loop; they
  are far faster than compiling per change.
- Do NOT trust `lake build` as a compile check: the `.lean` files here are not
  lake library targets, so `lake build` reports `Build completed successfully
  (0 jobs)` without ever compiling them. Always confirm with
  `lake env lean <file>`, which compiles the file by path.
- If a goal looks false or unprovable from the given hypotheses, re-read the
  statement: you likely misread a binder or a coercion. Do not "fix" it by
  changing the statement — finish the proof as stated.
- Non-trivial proofs routinely take many rounds of compile-error fixing. Keep
  iterating against the diagnostics rather than guessing."""
src/open_atp/harness/assets/scripts/kimi_agent.sh
#!/usr/bin/env bash

# $PROMPT is exported by the AgentProver before this script runs (it reads
# agent_prompt.txt from the workdir). The backend has already cd'd into the
# workdir and symlinked .lake to the warm Mathlib cache.
#
# KIMI_CODE_HOME is workdir-local so kimi's OAuth credential, provider config,
# the user-scope mcp.json (lean-lsp), the user-scope skills dir, and the
# per-session wire log all live under the workdir -- isolating concurrent runs
# and syncing the telemetry back out. `kimi -p` runs non-interactively and
# auto-approves tool calls (--yolo is rejected in prompt mode); the stream-json
# event stream goes to stdout.
#
# https://moonshotai.github.io/kimi-code/
#
# KIMI_DISABLE_CRON / KIMI_CODE_NO_AUTO_UPDATE stop kimi from spawning its
# background cron daemon and auto-updater: in an ephemeral sandbox those do
# unwanted network/CPU work and can self-modify the CLI mid-run, and a lingering
# child destabilizes a short-lived Modal sandbox (it outlives the `-p` exit).
#
# `kimi -p` has no effort flag, and config.toml's [thinking] effort is ignored for
# models that declare no `support_efforts` (the coding models don't -- only k3
# does). KIMI_MODEL_THINKING_EFFORT is the one lever that bypasses that gate; the
# value reaches the API as `reasoning_effort` and is validated server-side (an
# unsupported one fails the run with a 400).

export KIMI_CODE_HOME="$PWD/.kimi-home"
export KIMI_DISABLE_CRON=1
export KIMI_CODE_NO_AUTO_UPDATE=1
export KIMI_MODEL_THINKING_EFFORT='<<EFFORT>>'
kimi -p "$PROMPT" \
    --model '<<MODEL>>' \
    --output-format stream-json

Tracking cost and usage

The Kimi Code CLI does not report per-run USD, and its stream-json output carries only messages and tool calls, not token totals. Token totals are read from Kimi’s per-session wire.jsonl (usage.record events) synced back from the workdir-local KIMI_CODE_HOME, and the pricing table in COST_PER_MTOK is used to compute the cost in USD. This populates cost_usd in ProofResult. Usage within your plan’s quota is not billed. You can monitor plan consumption at Kimi Console.