| --- |
| title: AProver |
| emoji: 🛡️ |
| colorFrom: indigo |
| colorTo: blue |
| sdk: docker |
| app_port: 7860 |
| pinned: false |
| license: mit |
| short_description: Chat with an agentic model checker for C |
| --- |
| |
| # AProver — chat demo |
|
|
| Web front-end that lets visitors run [AProver](https://github.com/agentic-prover/aprover) by chatting, without configuring the tool. |
|
|
| The Space packages: |
|
|
| - the `bmc_agent` pipeline (Phase 1: spec gen → Phase 2: CBMC → Phase 3: CEx classify + refine → bug report), |
| - a FastAPI server (`web/server.py`) exposing `POST /chat` as a Server-Sent Events stream, |
| - a single-page chat UI (`web/static/`) that streams pipeline progress live. |
|
|
| ## How the chat works |
|
|
| The assistant is a Claude model with one tool, `run_aprover(source_code, function?, domain_knowledge?)`. When you paste C code, the model decides whether to call the tool, the server runs the pipeline in a worker thread, and every log line + final bug summary streams back into the chat as it happens. |
|
|
| **Bring your own key.** Visitors paste their own Anthropic API key into the UI; it is kept in browser `localStorage` and sent only as the `X-Anthropic-Key` header on their own requests, never stored server-side. Both the chat agent and the AProver pipeline run on the caller's key, so the host carries no per-visitor LLM cost. A server-side `ANTHROPIC_API_KEY` is optional and used only as a local-dev fallback. |
|
|
| Defaults are tuned for a public demo (no dynamic validation, short refinement loop, 60s CBMC timeout, 64KB source cap). Heavier configs are available via the CLI. |
|
|
| ## Running it locally |
|
|
| ```bash |
| # from the repo root |
| uv pip install fastapi "uvicorn[standard]" |
| ANTHROPIC_API_KEY=sk-... uv run uvicorn web.server:app --port 7860 |
| # then open http://localhost:7860 |
| ``` |
|
|
| CBMC must be on `PATH` (`apt install cbmc` on Debian/Ubuntu). |
|
|
| ## Deploying to Hugging Face Spaces |
|
|
| HF Spaces wants `Dockerfile` and `README.md` (with `sdk: docker` frontmatter) at the repo root, but the AProver repo already has a project README. Use the staging script: |
|
|
| ```bash |
| # 1. create an empty Space (SDK: Docker) on huggingface.co/spaces |
| # 2. clone it locally |
| git clone https://huggingface.co/spaces/<you>/aprover ~/aprover-space |
| |
| # 3. stage a Space-ready tree from this repo |
| ./web/deploy_to_space.sh ~/aprover-space |
| |
| # 4. push |
| cd ~/aprover-space && git add -A && git commit -m "Update AProver Space" && git push |
| ``` |
|
|
| No secrets are required: visitors supply their own Anthropic key in the UI (see "Bring your own key" above). Optionally set `BMC_AGENT_LLM_MODEL` (defaults to `claude-sonnet-4-6`), or `ANTHROPIC_API_KEY` as a fallback for local dev. The container listens on port 7860, which Spaces routes automatically. |
|
|
| ## Files |
|
|
| | Path | Purpose | |
| |------|---------| |
| | `web/server.py` | FastAPI app, `/chat` SSE endpoint, Claude tool-use loop | |
| | `web/runner.py` | Threaded wrapper around `AMCPipeline` that yields progress events | |
| | `web/static/` | Single-page chat UI (HTML + CSS + JS, no build step) | |
| | `web/Dockerfile` | Container image: python + cbmc + uv + project | |
|
|
