README.md

metadata

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 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

# 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:

# 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