KeYmaera X API Server for Agent Harnesses

WARNING: the README is slop. Instructions about how to use the infra are probably correct but statements about the tool itself seem meh.

A Docker container providing a REST API for AI agents to interact with KeYmaera X, a theorem prover for hybrid systems. Agents can submit models and proof scripts, then receive structured feedback on proof results.

What is This For?

This API enables AI agent harnesses to:

1. Verify hybrid system models - Submit .kyx files containing differential dynamic logic (dL) specifications
2. Execute proof scripts - Run Bellerophon tactic scripts to prove safety properties
3. Get structured feedback - Receive agent-friendly JSON responses with success/failure status, hints for fixing issues, and detailed proof metrics

KeYmaera X proves properties about cyber-physical systems - systems with both discrete (software) and continuous (physical) dynamics. Example applications include autonomous vehicles, aircraft collision avoidance, and medical devices.

Quick Start

# Build the Docker image
docker build -t keymaerax-api .

# Run the container
docker run -p 8080:8080 keymaerax-api

# Test it works
curl http://localhost:8080/health

The API will be available at http://localhost:8080.

Helper Scripts

./build.sh   # Build the Docker image
./run.sh     # Build (if needed) and run the container

Docker Compose

# Older Docker versions
docker-compose up --build

# Docker 20.10+
docker compose up --build

Important: Startup Overhead

Each proof request takes ~2 minutes due to KeYmaera X JVM startup and lemma derivation. This is inherent to KeYmaera X architecture - the theorem prover derives foundational lemmas at startup.

Plan your agent's timeout and retry logic accordingly.

API Reference

POST /prove/sync - Submit Proof (Synchronous)

Recommended for most use cases. Submit a .kyx file and wait for the result.

Request:

curl -X POST http://localhost:8080/prove/sync \
  -H "Content-Type: application/json" \
  -d '{
    "kyx": "ArchiveEntry \"Test\"\nProgramVariables Real x; End.\nProblem x>=0 -> [x:=x+1;] x>=1 End.\nTactic \"Proof\" implyR(1); assignb(1); QE End.\nEnd.",
    "timeout": 60
  }'

Parameters:

Field	Type	Required	Description
kyx	string	Yes	The .kyx file content
timeout	int	No	Proof timeout in seconds (default: 120, max: 600)

Response (success):

{
  "job_id": "abc-123",
  "success": true,
  "status": "completed",
  "message": "All proof entries completed successfully.",
  "entries_summary": [
    {"name": "Test", "proved": true, "steps": 38}
  ]
}

Response (unfinished proof):

{
  "job_id": "abc-123",
  "success": false,
  "status": "completed",
  "message": "1 of 1 entries did not complete.",
  "action_required": "Review unfinished entries and strengthen tactics.",
  "unfinished_entries": [
    {
      "name": "Test",
      "result": "unfinished",
      "hint": "The tactic did not close all proof branches. Consider: (1) strengthening loop invariants, (2) adding differential cuts for ODEs, (3) using 'ODE(1)' for automatic ODE reasoning."
    }
  ]
}

Response (parse error):

{
  "job_id": "abc-123",
  "success": false,
  "status": "completed",
  "message": "The .kyx file contains syntax errors.",
  "action_required": "Fix the parse error and resubmit.",
  "parse_error": {
    "line": 8,
    "column": 22,
    "type": "term",
    "found": ";] x >= 1",
    "expected": "number | dot | function | variable | termList | \"-\""
  },
  "fix_hint": "Ensure assignments end with semicolons: 'x := e;'"
}

POST /prove - Submit Proof (Asynchronous)

Submit a proof and poll for results. Useful for long-running proofs.

Request:

curl -X POST http://localhost:8080/prove \
  -H "Content-Type: application/json" \
  -d '{"kyx": "...", "timeout": 120}'

Response:

{
  "job_id": "abc-123",
  "status": "pending",
  "message": "Proof submitted. Poll /status/{job_id} for results."
}

GET /status/{job_id} - Check Proof Status

Request:

# Agent-friendly summary (default)
curl http://localhost:8080/status/abc-123

# Full details including raw KeYmaera X output
curl http://localhost:8080/status/abc-123?format=full

Response (running):

{
  "job_id": "abc-123",
  "status": "running",
  "message": "Proof is running (elapsed: 45.2s)",
  "success": false
}

Response (completed): Same format as /prove/sync response.

POST /parse - Validate Syntax

Check .kyx syntax without running proofs. Note: This also has ~2 minute startup overhead.

Request:

curl -X POST http://localhost:8080/parse \
  -H "Content-Type: application/json" \
  -d '{"kyx": "..."}'

Response:

{
  "valid": true,
  "message": "File parsed successfully"
}

GET /jobs - List Recent Jobs

curl http://localhost:8080/jobs?limit=10

Response:

{
  "jobs": [
    {
      "job_id": "abc-123",
      "status": "completed",
      "created_at": 1234567890.123,
      "overall_result": "proved"
    }
  ]
}

GET /health - Health Check

curl http://localhost:8080/health

Response:

{
  "status": "healthy",
  "service": "keymaerax-api"
}

GET / - API Documentation

Returns a JSON summary of available endpoints.

.kyx File Format

KeYmaera X uses .kyx archive files containing models and proofs in differential dynamic logic (dL):

ArchiveEntry "Entry Name"

ProgramVariables
  Real x;    /* Position */
  Real v;    /* Velocity */
End.

Definitions
  Real g;    /* Gravity constant */
End.

Problem
  x >= 0 & v >= 0 -> [x := x + v;] x >= 0    /* Safety property */
End.

Tactic "Proof Strategy"
  implyR(1); assignb(1); QE    /* Bellerophon tactics */
End.

End.

Key Components

Block	Purpose
ProgramVariables	Declare state variables (all Real)
Definitions	Constants, functions, predicates, hybrid programs
Problem	The dL formula to prove
Tactic	Bellerophon proof script

Common Tactic Patterns

/* Propositional */
implyR(1)              /* Decompose implication on right */
andR(1)                /* Split conjunction on right */
id                     /* Close by matching antecedent/succedent */

/* Hybrid programs */
assignb(1)             /* Handle [x:=e] assignment */
composeb(1)            /* Split [a;b] sequential composition */
loop("inv", 1)         /* Apply loop invariant */

/* ODEs */
ODE(1)                 /* Automatic ODE reasoning */
dI(1)                  /* Differential invariant */
dC("fact", 1)          /* Differential cut */

/* Arithmetic */
QE                     /* Quantifier elimination (sends to Z3) */

Agent Integration

Recommended Workflow

1. Submit proof with /prove/sync (simplest approach)
2. Check success field - true means all entries proved
3. On failure, read action_required and hint fields for guidance
4. Iterate on the proof script based on feedback

Python Client Example

import requests

class KeYmaeraXClient:
    def __init__(self, base_url="http://localhost:8080"):
        self.base_url = base_url

    def prove(self, kyx_content: str, timeout: int = 120) -> dict:
        """Submit a proof and wait for result."""
        response = requests.post(
            f"{self.base_url}/prove/sync",
            json={"kyx": kyx_content, "timeout": timeout},
            timeout=timeout + 200  # Account for startup overhead
        )
        return response.json()

    def is_healthy(self) -> bool:
        """Check if the API is available."""
        try:
            r = requests.get(f"{self.base_url}/health", timeout=5)
            return r.status_code == 200
        except:
            return False

# Usage
client = KeYmaeraXClient()

result = client.prove('''
ArchiveEntry "Simple"
ProgramVariables Real x; End.
Problem x >= 0 -> [x := x + 1;] x >= 1 End.
Tactic "Proof" implyR(1); assignb(1); QE End.
End.
''')

if result["success"]:
    print("Proof completed!")
    for entry in result.get("entries_summary", []):
        print(f"  {entry['name']}: {entry['steps']} steps")
else:
    print(f"Proof failed: {result['message']}")
    if "action_required" in result:
        print(f"Action: {result['action_required']}")
    if "unfinished_entries" in result:
        for entry in result["unfinished_entries"]:
            print(f"  {entry['name']}: {entry['hint']}")
    if "parse_error" in result:
        pe = result["parse_error"]
        print(f"  Parse error at line {pe.get('line')}, col {pe.get('column')}")

Handling the Startup Overhead

Since each request takes ~2 minutes, consider:

1. Batch multiple entries in a single .kyx file
2. Set appropriate timeouts in your HTTP client (at least 3 minutes)
3. Use async endpoint for very long proofs and poll periodically

Configuration

Environment variables for the container:

Variable	Default	Description
DEFAULT_TIMEOUT	120	Default proof timeout in seconds
MAX_TIMEOUT	600	Maximum allowed timeout
STARTUP_OVERHEAD	180	Buffer added for JVM startup
KEYMAERAX_JAR	/app/keymaerax.jar	Path to KeYmaera X JAR
WORKDIR	/app/workdir	Directory for temp files

Example with custom config:

docker run -p 8080:8080 \
  -e DEFAULT_TIMEOUT=300 \
  -e MAX_TIMEOUT=900 \
  keymaerax-api

Troubleshooting

Proof Times Out

The timeout parameter controls only the proof time, not the total request time. Total time = startup (~2 min) + proof time.

Solutions:

• Increase timeout: {"timeout": 300}
• Simplify proof with intermediate lemmas using cut("fact")
• Use hideL(-n) to remove unnecessary hypotheses before QE
• Replace master automation with manual proof steps

QE Fails or is Slow

Z3 is less powerful than Mathematica for real arithmetic. For complex quantifier elimination:

• Break into smaller steps: cut("x > 0"); <(QE, ...)
• Remove unused hypotheses: hideL(-1); hideL(-2); QE
• Add explicit bounds as assumptions in your model

Parse Errors

The response includes line/column information. Common issues:

Error	Fix
Missing semicolon	Assignments need ;: x := e;
Brace mismatch	Check {...}* for loops
Wrong arrow	Use -> not => for implication
Undefined variable	Declare in ProgramVariables block

Container Issues

# Check container logs
docker logs keymaerax-api

# Verify Java and Z3 work
docker exec keymaerax-api java -version
docker exec keymaerax-api z3 --version

# Test KeYmaera X directly
docker exec keymaerax-api java -jar /app/keymaerax.jar -help

Architecture

┌─────────────────────────────────────────────────────────┐
│                    Docker Container                      │
│  ┌─────────────────────────────────────────────────┐   │
│  │              Flask API (server.py)               │   │
│  │  - /prove/sync, /prove, /status, /parse, etc.   │   │
│  └──────────────────────┬──────────────────────────┘   │
│                         │                               │
│                         ▼                               │
│  ┌─────────────────────────────────────────────────┐   │
│  │           KeYmaera X (keymaerax.jar)            │   │
│  │  - JDK 17 runtime                               │   │
│  │  - Spawned as subprocess per request            │   │
│  └──────────────────────┬──────────────────────────┘   │
│                         │                               │
│                         ▼                               │
│  ┌─────────────────────────────────────────────────┐   │
│  │                 Z3 Solver                        │   │
│  │  - System package (ARM/x86 compatible)          │   │
│  │  - Used for quantifier elimination (QE)         │   │
│  └─────────────────────────────────────────────────┘   │
└─────────────────────────────────────────────────────────┘

Limitations

1. ~2 minute startup overhead per request (KeYmaera X JVM + lemma derivation)
2. Z3 only - no Mathematica support (Z3 is less powerful for some arithmetic)
3. Some derived lemmas fail with Z3 (23 of them), but basic proofs still work
4. In-memory job storage - jobs are lost on container restart
5. Single worker - requests are processed serially

License

This API wrapper is provided as-is. KeYmaera X is developed by the Logical Systems Lab at Carnegie Mellon University.

Links

• KeYmaera X Documentation
• Differential Dynamic Logic
• Bellerophon Tactics