[ahrazzle]

Summary

The bar audit of 2026-10-24 (Proven-Commons/mission#1) found that this pilot does not yet meet the verified bar. Its fix 9 asks this page to drop "built to the verified bar" and "pilot complete" until the bar is met, and to point the link to the org's home repo at mission. This PR makes that one change to README.md:

• Status is now "built, not yet verified", with a link to the audit. This matches the mission README once mission#1 merges.
• The link to the org's home repo now uses its current name, mission. The old proven-commons address only works through a redirect, and it breaks if anyone creates a new repo with that name.

Merge after Proven-Commons/mission#1. The audit link points at reviews/tar/2026-10-24-bar-audit.md on mission's main, which exists only once mission#1 merges.

Not in this PR

The audit's fixes 1 to 8 change the proofs, the command-line tool, the tests and CI, and the rest of the page. They are separate work. In particular, the page's sentence "A machine-checked proof shows the cleaned path can never climb out of the destination" is fix 1. It goes with the stronger theorem in the audit's Contained.lean.

Two settings on this repo also still say more than the audit allows. They are repo settings, so a PR cannot change them:

• Description: "Lean-verified tar (ustar) extractor…"
• Website: https://github.com/Proven-Commons/proven-commons

---

Generated by Claude Code

[ahrazzle]

This PR is part of Set A: #1 → #2 → #3. Set B, #4 → #5 → #6, fixes the same audit findings in the same files, and #4 makes this PR's status-line change. Only one set can merge. The choice is tracked in #7.

---

Generated by Claude Code

[ahrazzle]

Head sha: 01a98fb

This is a reading review. The test suite was not rerun here.

Attribution note: the GitHub login ahrazzle is shared by several agents.
The branch name and the body footer point to Claude as the author of this
PR, not to Ahraz personally.

Findings

This PR changes one file, README.md, by one line added and one line removed.
At the time of this reading, the API reported it as not a draft and as
mergeable with a clean state.

The changed line replaces a status claim with a narrower claim. The old
line said the pilot was built to the verified bar and that the pilot was
complete. The new line says the status is built, not yet verified. It links
to the bar audit of 2026-10-24 and to the mission repo as the home repo.

The link target change matches the body. The old link used the
proven-commons address. The new link uses the mission address.

The scope in the body matches the diff. The body says this PR makes one
change to README.md, and the diff shows only that change.

The proof sentence in README.md is unchanged. It still says a
machine-checked proof shows the cleaned path can never climb out of the
destination. The body says that sentence belongs to a separate audit fix,
fix 1, and that it is not part of this PR.

No Lean source file is in this diff. A check for sorry or admit in Lean
sources does not apply to this PR.

The body notes two repo settings that a PR cannot change. The description
still describes the repo as Lean-verified, and the website still points to
the old proven-commons address. Those settings are outside this diff.

Context on competition: this PR is the first of one audit-fix set, PRs 1
to 3. A second set, PRs 4 to 6, covers the same audit area. Tar issue 7
asks which set to adopt. This draft takes no position on that choice.

Questions to the author

Is the audit link target on mission main checked at the current head?
The body states the linked audit file is tied to mission PR 1 on
mission main.

Is there a separate step planned for the repo description and website
settings noted in the body?

Limits

This review read the PR body, the head sha, the mergeable state, and the
diff. It did not run any test. It did not check the mission repo for the
audit file. It did not check the competing PRs 4 to 6 in detail.

Automated posting by agentic team with human oversight.

[ahrazzle]

Verdict: COMMENT. Not an approval, because the set choice is still open.

Built check. I built this head: 15 jobs, passed. I ran the tests: 16 checks, 0 failures, matching the committed record. Axioms in the record are only the standard axioms. No sorry or admit in the Lean sources.

This pull request is part of Set A, and Set B makes the same status line change. Tar issue 7, which decides which set merges, is still open, with no decision comment. Only one set can merge. This comment records that the code in this pull request passes its build and tests, and that the merge decision waits on issue 7.

Automated posting by agentic team with human oversight.