Metadata-Version: 2.4
Name: keymaerax
Version: 0.3.0
Summary: CLI tool to run KeYmaera X theorem prover as a Docker-based API service
Project-URL: Homepage, https://github.com/keymaerax/keymaerax-api
Project-URL: Documentation, https://github.com/keymaerax/keymaerax-api#readme
Project-URL: Repository, https://github.com/keymaerax/keymaerax-api
Author: Nathan Fulton
License-Expression: MIT
Keywords: api,docker,formal-verification,keymaerax,theorem-prover
Classifier: Development Status :: 4 - Beta
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Testing
Requires-Python: >=3.9
Requires-Dist: docker>=7.0.0
Requires-Dist: httpx>=0.27.0
Requires-Dist: mcp>=1.0.0
Description-Content-Type: text/markdown

# 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](https://keymaerax.org/), a theorem prover for hybrid systems. Agents can submit models and proof scripts, then receive structured feedback on proof results.

# 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

# 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

## Quick Start

```bash
# 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

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

### Docker Compose

```bash
# Older Docker versions
docker-compose up --build

# Docker 20.10+
docker compose up --build
```

## API Reference

### `POST /prove/sync` - Submit Proof (Synchronous)

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

**Request:**
```bash
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):**
```json
{
  "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):**
```json
{
  "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):**
```json
{
  "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:**
```bash
curl -X POST http://localhost:8080/prove \
  -H "Content-Type: application/json" \
  -d '{"kyx": "...", "timeout": 120}'
```

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

### `GET /status/{job_id}` - Check Proof Status

**Request:**
```bash
# 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):**
```json
{
  "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:**
```bash
curl -X POST http://localhost:8080/parse \
  -H "Content-Type: application/json" \
  -d '{"kyx": "..."}'
```

**Response:**
```json
{
  "valid": true,
  "message": "File parsed successfully"
}
```

### `GET /jobs` - List Recent Jobs

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

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

### `GET /health` - Health Check

```bash
curl http://localhost:8080/health
```

**Response:**
```json
{
  "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

```python
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:
```bash
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

```bash
# 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)         │   │
│  └─────────────────────────────────────────────────┘   │
└─────────────────────────────────────────────────────────┘
```

