Proofrun answers "does this repository actually do what its README says?" — by checking the code and running focused tests when needed.
You ask a question about a repository. It decides whether reading settles the matter or whether it has to clone the code and execute it in a sandbox, then answers with a ledger where every claim names a source tool and is tagged by what kind of evidence it is.
Open the local UI with two switchable modes. Monitoring surfaces saved investigations from the automatic discovery pipeline: what was checked, what was found, and what remains unknown. Ask it yourself accepts a GitHub repository URL and a question in separate fields. It can also reopen past questions saved in local SQLite without starting another investigation.
Monitoring: The completed 2026-W39 batch shows an inconclusive Langfuse investigation with its evidence and limits. Other discovered repositories are listed separately as Not investigated.
Ask it yourself: A direct question asks whether Engram can save a fact to SQLite, reopen the file, and recall it without an API key. The saved local run 52 tested one fact and query in Docker and returned supported. The answer shows what was checked and what remains unknown; the expanded report shows the sandbox evidence. This direct run is local and is not in the published weekly feed.
The live GitHub Pages site publishes the latest completed weekly batch for browsing without the local app. The historical investigation traces remain available separately. Pages is a static showcase; direct questions run in the local Streamlit app.
Use Python 3.11. Browsing the recorded examples and published weekly results does not require an API key or Docker.
python3.11 -m venv .venv
source .venv/bin/activate
python -m pip install -r requirements.txt
python -m streamlit run app.pyOpen Monitoring for the weekly results or Ask it yourself to view a saved question. A new investigation is a separate paid action; see live-run setup before pressing Investigate.
The monitoring tab reads discovery-linked investigation results from local SQLite and the public weekly feed without starting an investigation. If none exist, it shows three clearly labeled recorded investigations initiated by direct questions, demonstrating the same investigation engine. These examples work without credentials, Docker, or a local database. Earlier discovery summaries remain in a secondary section. An Also discovered section lists the other repositories from the latest completed weekly batch, with descriptions and links, labeled Not investigated. The weekly workflow uses the existing Claude API: Haiku scores up to ten discoveries and Sonnet investigates at most one. See weekly monitoring setup for activation and current publication status. The Gemini evaluation remains historical comparison evidence.
Results lead with a short answer and understandable findings. Original reports, evidence sources, commands, review issues, and execution costs remain available under “Full report, sources, and execution details.” New reports also include explicit limitations, reviewed alongside the conclusion, without an additional model call. Existing stored reports remain readable.
The Investigate button runs a new question locally and saves its result to
SQLite. Live use needs ANTHROPIC_API_KEY; Docker and the sandbox image are
needed when the agent executes repository code. The displayed spend allowance
and token cost are estimates. A repeated submission in the same UI session
shows the previous outcome until you explicitly allow another run.
Ask about one repository:
python investigate.py "Is firecrawl/firecrawl licensed under terms that would \
oblige a company embedding it in a hosted product to publish their source?"VERDICT SUPPORTED
SUMMARY The repository is confirmed via both GitHub's license metadata
and the actual LICENSE file text to be licensed under AGPL-3.0.
The LICENSE file content retrieved was truncated before the
specific clause requiring network server operators to provide
source code [...] The verdict of 'supported' rests on correct
identification of the license type rather than on a verified
quotation of the specific clause.
3 steps, stop=sufficient_info, 0 observed / 1 inspected / 1 reported
estimated token cost $0.1087, 24s
Or run the whole question set and score it:
python investigate_batch.py --questions questions.yaml \
--out reports/batch.md --budget 6
python evaluate.py --investigationsProofrun eval: 10/13 questions pass
estimated token cost $4.92, 24 min, 15 observed / 15 inspected / 33 reported
Asked whether microsoft/apm really turns an apm.yml manifest into configured
agent files with one command, it read the metadata, decided it had to run the
thing, and built its own test case:
s3 sandbox_clone() git clone --depth 1 → 54.8 MB
s4 sandbox_setup(pip install -e .) 24.4s, exit 0 → apm-cli 0.30.0
s5 sandbox_run(apm compile ...) ERROR
s9 sandbox_run(write a minimal apm.yml ← its own test case, from scratch
in an empty dir, compile it)
s10 sandbox_run(cat AGENTS.md; find .) ← did the file really appear?
s11 sandbox_run(copy only the manifest ← does it reproduce away from
to a third dir, recompile) the repo that claimed it?
verdict: supported · 12 steps · estimated token cost $0.475 · 87s
Nobody told it to design that experiment. It wrote a manifest in an empty directory, compiled it, confirmed the output appeared, then copied only the manifest somewhere unrelated and compiled again — testing whether "one file reproduces it everywhere" survives leaving the repository that said it.
Full trace, ledger and critique · historical runs and traces
Ask it yourself. One question, one repository, answer on stdout and in the database.
python investigate.py "Does owner/name actually ...?"Or let the monitor ask. The sequential pipeline fetches arXiv, GitHub and
Hacker News items, scores them against your interest areas, and writes a themed
brief from up to 100 stored scored items across all dates. Repositories that
score well get a question derived from their README, and the investigation
agent answers it. The brief does not incorporate those investigation verdicts.
--agent instead runs a lighter read-only repo agent. --graph runs the
watchers in parallel but does not support either agent or --skip-fetch.
The weekly workflow discovers up to 10 repositories and investigates at most
one, with a shared UI/Pages feed. It uses the Claude API and requires explicit
repository activation variables.
With Anthropic, direct questions and the weekly investigation use Sonnet; Haiku scores the weekly discoveries and is used by the legacy monitor's automatic investigation path. Sonnet writes the brief. Ollama uses the selected local model for analysis and synthesis; automatic investigation requires Anthropic's web-search support and the local Docker sandbox.
python run.py --investigate --investigate-threshold 0.6Every claim carries a kind and a source tool name:
| Kind | Means |
|---|---|
observed |
a command ran in the sandbox and exercised the thing |
inspected |
a fact GitHub computed — licence, language, which files exist |
reported |
somebody's prose, including the project's own |
Three rules then run in code, after the model has answered:
- A claim citing a tool name absent from the trace is dropped.
- A claim can never be stronger than the tool it cites. Reading a file is not running one.
- A verdict of supported or refuted needs at least one first-hand claim, or it drops to inconclusive.
That last rule is what makes a hostile README expensive. It can tell the model
to report a claim as proven, and the model may comply — but its text can only
ever be reported, so the verdict cannot reach supported without something
the agent actually did.
The ledger validates tool names and caps evidence kinds by tool. It does not bind an entry to the exact invocation or prove that output supports the claim. Review the trace and output when the distinction matters.
There are no confidence scores. Why, and what it costs.
- Run anything but Python. The container has python, pip, git, curl and a C toolchain. A Rust or Go repository is refused before it is cloned.
- Reproduce a benchmark. "Fifty times faster than X" needs both systems and a load generator. It will tell you it cannot check that, rather than guess.
- Pretend. When it cannot answer, it says
could_not_testand names what stopped it.
10 of 13 recorded questions pass every criterion, at about $4.92 estimated token cost and 24 minutes of recorded runtime for the full set.
| run 1 | run 2 | run 3 | |
|---|---|---|---|
| passing | 6/13 | 8/13 | 10/13 |
| estimated token cost | $4.98 | $4.31 | $4.92 |
No pass has ever regressed, and no question has been edited after seeing results. The three that still fail are listed with their causes rather than omitted: the eval, in full.
The ladder. get_repo_metadata → get_repo_description → list_files →
read_file → web_search → sandbox_clone → sandbox_setup → sandbox_run.
It lives in the tool descriptions, not in code that forces an order — the model
picks the rung, and the eval scores whether it picked the right one.
The sandbox. Three verbs, each a fresh docker run --rm against one named
volume at /work:
| Verb | Network | Timeout |
|---|---|---|
sandbox_clone |
bridge | 300s |
sandbox_setup |
bridge | 300s |
sandbox_run |
none | 120s |
Plus --read-only, --user 1000:1000, --cap-drop ALL, --memory 2g,
--pids-limit 256, --env-file /dev/null. Network is a property of the verb,
not an argument the model can pass, and no environment ever crosses the
boundary. The repository under investigation comes from a public feed, so
anyone who can publish one can choose what this executes.
Threat model and alternatives.
The caps. Steps (20), loop token cost, wall clock (900s), sandbox calls (12, of which 4 may be setup), and disk (2 GB). Cost and wall clock are checked between model turns, so a call can overshoot. Disk is measured after a command, so that command can exceed the threshold before the agent stops. A cap that fires is scored as a failed run.
Cost control. A free keyword pre-filter before any model call; content-hash idempotency for unchanged analysis; and a batch budget checked against a per-question spend estimate before each question starts. Token costs use configured rates and usage counts, so they are estimates. The loop cap excludes the overshoot turn, wrap-up, extraction, critique and web-search charges; the batch estimate includes allowances for these but is not a guaranteed total-spend limit.
Architecture, the pipeline, and what is and isn't an agent here.
The local app setup above is enough to browse saved results. For a new direct
investigation, add an Anthropic API key to .env. Start Docker Desktop and
build the sandbox image when the question needs repository execution. Check
Docker before starting an execution-based run.
cp .env.example .env # add ANTHROPIC_API_KEY, optionally GITHUB_TOKEN
python check_api.py # verifies the key, generates no tokens
docker info # confirm the engine is running
docker build -t ai-monitor-sandbox:latest sandbox/ # one-time execution image
python -m pytest tests/ -q # offline suite; no network, Docker daemon, or API keyGetting an API key, and why the Console is separate from claude.ai: docs/api-setup.md.
site/ is a complete static site — no build step, no JavaScript, no external
assets. The weekly page is its landing page; the recorded evaluation index is
kept at history.html. To regenerate the historical traces locally:
python export_traces.py && open site/history.htmlGitHub Pages publishes through the weekly GitHub Actions workflow. That
workflow copies the historical files from gh-pages, refreshes the weekly
landing page and feed from the saved monitoring state, then deploys the combined
site. The gh-pages branch is retained as the historical asset source; it is
no longer the Pages publishing source. See weekly monitoring setup
for the schedule, activation variables, and state recovery procedure.
| decisions.md | Design decisions with revisit conditions, including ones later corrected |
| evidence-ledger.md | The three kinds, the three rules, and why there are no confidence scores |
| eval-investigations.md | The six criteria, three runs, and every failure |
| architecture.md | The pipeline, the loop, the layout, known limitations |
| testing.md | What the suite caught, and what it pins |
| eval-findings.md | Stage 1: the models agree with each other, not with the human |
| api-setup.md | Keys, the Console, and billing |
| release-notes.md | Portfolio release summary and limits |