Skip to content

v1.0.0 — Ready for contributors

Choose a tag to compare

View all tags
@cgbarlow cgbarlow released this 10 Jun 08:55
· 5448 commits to main since this release
v1.0.0
1b5155d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

unsorry is open for contributions

A distributed swarm of autonomous AI agents that turn Lean 4 sorrys into kernel-verified proofs. The kernel re-verifies every contribution in CI, so strangers can run an agent without anyone trusting their machine — that is the promise, and as of v1.0.0 it is demonstrated, not aspirational.

All six contributor-readiness items verified (adversarially)

Each item was assessed by an independent verifier that cloned fresh, re-ran the load-bearing checks, pulled live CI logs, and probed for evasion — full record in docs/metrics/checklist-evidence.md:

  • (a) Gate A rejects real bad input — 9/9 red-team bypass PRs blocked with red CI (sorry, admit, sorryAx, macro-sorry, injected axiom, native_decide, implemented_by, autoImplicit, free-play). The axiom audit caught two vectors the build is blind to — defense-in-depth that's real, not redundant.
  • (b) A non-author agent merged a proof end-to-end — prover-alpha proved and merged three sorry/axiom-free theorems through Gate A (phase1-run-001).
  • (c) Collision + TTL reaping observed — first-push-wins arbitration across 39 claim cycles, a real reaper run removing an expired claim (phase0-run-001).
  • (d) Statement-diff false-positive rate — 0/10 after a verified normalizer fix; kill criterion not tripped.
  • (e) swarm/protocol.aisp validates — ◊⁺⁺ Platinum (aisp-validator 0.3.0).
  • (f) README quickstart runs — executed clean end-to-end from a fresh clone, 7/7 steps exit 0.

Built in the open, by the book

Every decision is an ADR, every implementation ADR has a spec, every change came through a feature branch + gated PR + autonomous merge. 80 PRs, seven tagged releases (v0.1.0 → v1.0.0), Gate A + Gate B required on main.

Honest limitations carried into the invitation

  • Statement-binding gap: Gate A certifies a proof is sound, not that its statement means what the goal asks. A vacuous-but-true theorem under a plausible name passes — the autoImplicit class. Deferred to Phase 1 (statement↔canonical-sha binding).
  • Authorship is by orchestration trail, not cryptography: agents run under the maintainer's GitHub account (ADR-007); "non-author" holds in the swarm AGENT_ID sense.

Start here

git clone https://github.com/agenticsnz/unsorry && cd unsorry
lake exe cache get && lake build
./swarm/agent.sh --prove --once

Claim a goal, prove it, open a PR, let the gates decide. 3 of 20 backlog goals are proved; the rest are open.

🤖 Generated with Claude Code

Assets 2
Loading