key-agent-client

A Python client for the headless KeY theorem prover server — for proving that Java code satisfies its JML specification, and for finding out what to do when it does not.

This is a third-party tool. It is not an official KeY component.

It talks to a running keyext.server over JSON-RPC and does nothing else. It contains no Java, ships no jar and never starts a JVM: the server is a separate long-lived process, which is the whole reason it is worth talking to instead of re-running a prover from cold on every attempt.

Install

uv add key-agent-client        # or: pip install key-agent-client

No dependencies. Python 3.10 or newer. Add the [mcp] extra for the MCP server.

Start a server

This client does not start one, on purpose: a library that spawns JVMs is a library that owns processes it cannot supervise. keyext.server lives in this KeY fork — it is not part of upstream KeY — and every release there carries a prebuilt jar. Its name carries both KeY's version and the server's, so ask the release for it rather than writing it down:

gh release download --repo AzoteGwei/key --pattern 'keyext.server-*-exe.jar'
java -Xmx4g -jar keyext.server-*-exe.jar --port 0 --workspace /path/to/project

Or build it, from a checkout of that fork:

./gradlew :keyext.server:shadowJar
java -Xmx4g -jar keyext.server/build/libs/keyext.server-*-exe.jar \
  --port 0 --workspace /path/to/project

Give it -Xmx4g. KeY is memory-hungry and the default heap will not survive a real proof. The server publishes the port it got, so nothing needs to be passed to this client. The usage guide has the same download without gh, and the rest of the server's options.

Prove something

from keyclient import KeyClient

with KeyClient.discover(workspace="/path/to/project") as key:
    load = key.wait_for_task(key.load("/path/to/project").task_id)
    env = load.result["envId"]

    contract = key.obligations(env)[0].contract_id
    proof = key.start_proof(env, contract)
    key.wait_for_task(key.run_auto(proof, timeout_ms=60_000).task_id)

    stats = key.statistics(proof)
    print("closed" if stats.closed else f"{stats.open_goals} goal(s) still open")

Or from a shell:

key-agent load /path/to/project
key-agent prove env-1a2b3c4d 'Max[Max::max(int,int)].JML normal_behavior operation contract.0'
key-agent explain prf-9f8e7d6c

The one thing to know

Statistics.closed is the server's report of KeY's own Proof.closed(). It is the only value in this library that means a contract was proved. Nothing here computes it, infers it or defaults it.

In particular a finished task is not a closed proof: slow work returns a handle whose status becomes SUCCEEDED, meaning the work ran to an end. A macro that ends leaving three goals open is a succeeded task with three open goals.

Where to go next

The guide's vocabulary section is worth five minutes before anything else: the distinctions in it — finished versus closed, out of ideas versus out of budget — are the ones that get misread.

Releasing

Releases are cut by tag, and only a tag on main publishes anything.

1. Set the version in pyproject.toml and src/keyclient/__init__.py. tests/test_version.py fails if they disagree.
2. Merge that to main.
3. git tag -a v0.1.0 -m "…" && git push origin v0.1.0.

.github/workflows/release.yml then refuses the tag unless its commit is on main and its name matches pyproject.toml, builds, uploads to PyPI through a trusted publisher — no API token exists for this project — and opens a GitHub release with the wheel, the sdist and a summary. Both the PyPI upload and the attached files are attested; the release notes say how to check them.

Licence

MIT. The KeY server it talks to is GPL-2.0-only; this client is a separate program that communicates with it over a network protocol.