From 7a867d7a5cec2d28cf47b9df9b91ef61f3fbe475 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Sun, 25 Oct 2026 10:45:53 -0500 Subject: [PATCH 01/22] Add candidate list reference to README Added a candidate list section to the README. --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 4ad21e0..5fdfac0 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,8 @@ Pilot (complete): the tar extractor lives in its own repo, [tar](https://github. Wave 1: a policy engine in the style of AWS Cedar, a reader for the SQLite file format, and a parser for the Redis protocol with a small key-value store. +Candidate list: [CANDIDATES.md](CANDIDATES.md) holds every target, its score, its repo and plan, who claimed it, and its state. It is updated as targets ship and new candidates are proposed. + Each project sends reusable lemmas to CSLib and Mathlib, the shared libraries for computer science and mathematics in Lean. The shared library grows. The next project starts cheaper. ## Learn here From cf9591a148cf35112b9c44756f68212184042f6c Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Sun, 25 Oct 2026 10:46:29 -0500 Subject: [PATCH 02/22] Add CANDIDATES.md --- CANDIDATES.md | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 CANDIDATES.md diff --git a/CANDIDATES.md b/CANDIDATES.md new file mode 100644 index 0000000..9ef4c98 --- /dev/null +++ b/CANDIDATES.md @@ -0,0 +1,110 @@ +# Candidate list + +This file is the permanent record of targets for Proven Commons. It holds +every target in one place: what it is, how it scored, where its repo and +plan live, who is working on it, and what state it is in. + +The list changes as work moves. A target moves through these states: +proposed, repo created, claimed, in progress, shipped, maintained. When a +target ships, move its row to Shipped and keep its links. Do not delete +shipped rows. When a new candidate is identified, add it to Proposed with +its score, slice, claim, and oracle, before any repo is created. + +This file integrates the earlier list in mission issue 12 in full. All +eight targets from that issue appear below, with their scores and slices, +plus the Base32 note folded into the codec row. Issue 12 stays as history. +This file is the living list from here on. Do not maintain a second living +list in issue comments. Update this file when a status changes. + +## Scoring + +Score each candidate 0 to 3 on each point, total out of 18, as the founding +brief sets out. + +- Harm if it fails: money moved, access granted, data exposed, safety affected. +- Reach: how much other software depends on it. +- Specification size: a short public specification scores high. A large or + disputed one scores low. +- Oracle: an original implementation and test suite exist to compare against. +- Slice: a useful part can be cut out and proved on its own. +- Upstream stance: the maintainers will read a submission and give feedback. + +Scores for the mission issue 12 targets come from that issue. Scores for +the new candidates in Proposed come from the proposal dated 2026-10-25 and +await org confirmation. + +## Shipped + +| Target | Score | Repo | State | +| --- | --- | --- | --- | +| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Pilot complete. Proved rule: no file in an archive can be written outside the destination folder. Bar audit still open in mission issue 1, so do not call it verified until that audit closes. | + +## In progress + +| Target | Score | Repo | Plan | Claimed by | State | +| --- | --- | --- | --- | --- | --- | +| Codec: hex, Base64, CRC-32 | Academy material, not scored in issue 12 | [codec](https://github.com/Proven-Commons/codec) | [codec#1](https://github.com/Proven-Commons/codec/issues/1) | Claude (import), hyd-nawab (Base32) | Import in codec PR 1. Base32 in codec PR 2, stacked on PR 1. Base32 does not get its own repo. | +| ZIP archive reader | 15 | [zip](https://github.com/Proven-Commons/zip) | [zip#1](https://github.com/Proven-Commons/zip/issues/1) | hyd-nawab | Stored entries only, with a proved path gate. Draft PR 2 states 3,058 checks, 0 failures, seed 20261025. | +| JSON parser and printer (RFC 8259) | 16 | [json](https://github.com/Proven-Commons/json) | [json#1](https://github.com/Proven-Commons/json/issues/1) | hyd-nawab | First slice in progress. Round trip is the main claim. | +| RFC 3339 timestamp parser | 16 | [rfc](https://github.com/Proven-Commons/rfc) | [rfc#1](https://github.com/Proven-Commons/rfc/issues/1) | Claude | First slice in PR 2, ready for review. CI green, awaiting a spec reviewer. | +| Protobuf wire format codec | 15 | [protobuf](https://github.com/Proven-Commons/protobuf) | [protobuf#1](https://github.com/Proven-Commons/protobuf/issues/1) | Claude | First slice in PR 2, ready for review, after the RFC 3339 slice is up for review. Wire layer only. | +| WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice in draft PR 2. Round trip proved, 720 checks, 0 failures, seed 20261025. Longer length forms than needed are turned away. | +| CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | +| UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | + +## Repo created, work not started + +| Target | Score | Repo | Plan | State | +| --- | --- | --- | --- | --- | +| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | Plan names hyd-nawab for the first work. No claim comment has landed yet, so confirm the claim before starting. | + +## Planned, no repo yet (Wave 1) + +From the founding brief, months 4 to 9, one squad each. No scores published +for these three yet. + +- Policy engine in the style of AWS Cedar. Claims: a satisfied forbid gives + a deny, no satisfied permit gives a deny, and policy order does not change + the decision. +- SQLite file reader. Slice: 100-byte header, page header, and records. + Claims: the parser returns an error instead of reading outside the file, + and a record it reads stays inside its page. +- Redis protocol parser and small key-value store. Claims: reading what the + printer wrote gives the same command back, a get after a set returns the + set value, and a get after a delete returns nothing. + +## Proposed, no repo yet + +Proposed 2026-10-25 by amp-sai, agent for Ahraz Arifuddin. None of these +duplicates Wave 1, mission issue 12, tar, or codec. Org owners create a repo +only after confirming the score and slice. + +| Target | Score | Slice | Main claim | Oracle | +| --- | --- | --- | --- | --- | +| TOML 1.0 parser | 16 | Parse a TOML document into tables, arrays, strings, integers, floats, booleans, and datetimes. No printer in the first slice. | Parsing a document and reading a key back gives the value the document states, and a document outside the grammar is rejected. | Python tomllib, Rust toml crate, TOML test suite | +| IP address and CIDR parser | 16 | Parse IPv4 and IPv6 addresses and CIDR prefixes. No DNS lookup. | An address is inside a prefix exactly when its masked bits match the prefix bits. An address with an extra part, or a prefix length past the address size, is rejected. | Python ipaddress, Rust std IpAddr, RFC 4291 and RFC 4632 examples | +| HTTP/1.1 header parser | 15 | Parse a request line and headers only. No body, no chunked transfer, no server. | A header block is accepted exactly when it matches RFC 9112 framing rules. Duplicate Content-Length, a bare carriage return, and an obsolete folded line are rejected. | Python http.client in strict mode, httpbis test cases | +| MessagePack decoder | 15 | Decode MessagePack items with definite lengths: integers, strings, binary, arrays, and maps. No extension types in the first slice. | Decoding an encoding returns the same item, and the decoder returns an error instead of reading past the end of its input. | Python msgpack, official MessagePack test vectors | +| UUID parser | 15 | Parse the canonical text form in RFC 9562 and print it back. No generation in the first slice. | Print then parse returns the same UUID. A string with the wrong version or variant field, or a misplaced hyphen, is rejected. | Python uuid, Rust uuid, RFC 9562 examples | +| DNS wire message parser | 14 | Parse a DNS message header, questions, and records from RFC 1035 bytes, with compression pointers limited to earlier offsets in the same message. | The decoder never reads past the end of the message. A pointer loop, or a pointer forward in the message, is rejected. | Python dnspython, dig output for the same messages | +| Bencode parser | 13 | Parse integers, byte strings, lists, and dictionaries, with dictionary keys in sorted order. | Decoding an encoding returns the same value, and a dictionary with unsorted keys is rejected. | Python bencode libraries, torrent files in the wild | + +Kept on record, not proposed now: ELF header parser, scored 11. Its spec is +large and a first slice would still leave most of the format outside the +proof. Revisit it once the binary-format repos have a shared scaffold. + +## How this list is maintained + +- Claim rule: take work by leaving a comment on the plan issue that names + who is working on it, before starting. Update this file in the same change + where the claim, repo creation, draft PR, merge, or shipped state lands, + or in a follow-up PR that states the change. +- One row per target. A target that ships moves to Shipped with its repo and + project page links. A target that is split keeps its original row and adds + a row for the new part, with a note on the split. +- A new candidate joins Proposed only with all six scores, a slice, a main + claim, and an oracle. A candidate with no repo is not work to claim yet. +- Check this file against the plan issues before reusing a status in a + report. Plan issues and draft PRs change faster than this list. +- Mission issue 12 is history, not a second list. Its eight targets are + fully integrated above. Future status changes go here, not there. From 909f8d09341dd80e7b82c3637fb425d35d2c05ed Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 16:31:33 +0000 Subject: [PATCH 03/22] Candidates: third-round proposals, and the semver claim Add seven proposed targets with scores, slices, main claims and oracles: TLS host name matching, Punycode, Bech32, HPACK, DER, lexical path cleaning and URI resolution. Keep WebAssembly framing on record, and list follow-ons for codec and for lean-zip upstream. Move semver to In progress: hyd-nawab claimed it first, with a second draft slice after a claim 37 seconds later, and the choice left to a person. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 9ef4c98..0194d7c 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -51,12 +51,13 @@ await org confirmation. | WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice in draft PR 2. Round trip proved, 720 checks, 0 failures, seed 20261025. Longer length forms than needed are turned away. | | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | +| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | Plan names hyd-nawab for the first work. No claim comment has landed yet, so confirm the claim before starting. | +| (none at present) | | | | | ## Planned, no repo yet (Wave 1) @@ -93,6 +94,41 @@ Kept on record, not proposed now: ELF header parser, scored 11. Its spec is large and a first slice would still leave most of the format outside the proof. Revisit it once the binary-format repos have a shared scaffold. +Proposed 2026-10-25 by fdn-claude, agent for the fdn-0 account. None of +these duplicates a repo, Wave 1, the rows above, or codec. The scores are a +first pass from one agent and await a second scorer and org confirmation. +The full sheet, with the reasons for each score and sources, is in the pull +request that added these rows. + +| Target | Score | Slice | Main claim | Oracle | +| --- | --- | --- | --- | --- | +| TLS host name matching (RFC 9525, section 6.3) | 17 (H3 R3 S3 O3 Sl3 U2) | Match a reference DNS name against a presented name: ASCII names and A-labels, one wildcard as the whole left-most label. No certificate parsing. | A wildcard matches exactly one left-most label and nothing else; two wildcards, a partial wildcard such as f*.example.com, or a wildcard outside the left-most label match nothing; ASCII case is the only difference ignored. | x509-limbo webpki cases, OpenSSL X509_check_host with no partial wildcards, Go VerifyHostname, pyca/cryptography | +| Punycode (RFC 3492) | 16 (H2 R3 S3 O3 Sl3 U2) | Encode and decode one label, with the overflow checks of section 6.4. No IDNA mapping. | Decoding an encoding gives the code points back; the decoder accepts only the encoder's outputs, up to ASCII case; it fails at the overflow bound instead of wrapping. | RFC 3492 section 7.1 samples, Python punycode codec, npm punycode, libidn2. Python accepts "-tda" where the RFC decoder and npm punycode reject it. | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | +| HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | +| ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | +| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | +| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | + +Kept on record from the same sheet, not proposed now: WebAssembly module +framing, scored 13. The harm in a framing slice is low, and Vest (Verus) +and WasmCert (Isabelle, Coq) already cover the ground. + +Follow-ons from the same sheet, not new repos: + +- Into codec: PEM (RFC 7468) on top of the proved Base64; percent-encoding + (RFC 3986, section 2.1), which uri would import; and Luhn and IBAN mod + 97-10 check digits as Level 0 items next to CRC-32. The IBAN pair makes a + good lesson: its error detection holds inside runs of digits and of + letters, and fails across them ("B1" and "1B" both become "111"). +- Upstream, not here: DEFLATE inflate (RFC 1951) and gzip framing (RFC + 1952) already have a pure Lean implementation with a proved round trip in + kim-em/lean-zip. The gaps worth offering there are correctness against + RFC 1951 for any encoder's stream, the gzip trailer, and the output bound. + lean-zip runs a few C primitives in place of what it proves, which bar v2 + forbids, so using it here needs an org decision. The same author's + lean-archive reads tar and ZIP; the tar and zip repos should know of it. + ## How this list is maintained - Claim rule: take work by leaving a comment on the plan issue that names From 658181e7858794abe5fd1e215f6d0e83f3ac4794 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:59:35 +0000 Subject: [PATCH 04/22] Candidates: second score for round 3; hostname claimed, punycode repo made The second scorer agreed with every round 3 score except punycode's, which moves from 16 to 15 (Oracle 2, because the oracles disagree on "-tda"). Hostname moves to In progress, claimed on hostname#1. Punycode moves to Repo created. The uri row now says its first slice needs no escape handling, and the path row records the placement note. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 0194d7c..56023d7 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -52,12 +52,13 @@ await org confirmation. | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | +| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. The plan records three choices RFC 9525 leaves open: wildcards over a public suffix, a trailing dot, and label syntax. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| (none at present) | | | | | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | None yet | Repo created 2026-10-26. Slice as proposed: encode and decode one label, with the overflow checks of section 6.4. The second scorer set Oracle to 2 because the oracles disagree on "-tda". The harness counts that case on its own, with RFC 3492 as the reference. | ## Planned, no repo yet (Wave 1) @@ -95,20 +96,20 @@ large and a first slice would still leave most of the format outside the proof. Revisit it once the binary-format repos have a shared scaffold. Proposed 2026-10-25 by fdn-claude, agent for the fdn-0 account. None of -these duplicates a repo, Wave 1, the rows above, or codec. The scores are a -first pass from one agent and await a second scorer and org confirmation. -The full sheet, with the reasons for each score and sources, is in the pull -request that added these rows. +these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, +the ahrazzle account, scored each target on its own on 2026-10-26. They +agreed with every score but punycode's, which went from 16 to 15. The full +sheet, the reasons for each score, the sources and the second score are in +the pull request that added these rows. Hostname and punycode now have +repos, so their rows have moved up. | Target | Score | Slice | Main claim | Oracle | | --- | --- | --- | --- | --- | -| TLS host name matching (RFC 9525, section 6.3) | 17 (H3 R3 S3 O3 Sl3 U2) | Match a reference DNS name against a presented name: ASCII names and A-labels, one wildcard as the whole left-most label. No certificate parsing. | A wildcard matches exactly one left-most label and nothing else; two wildcards, a partial wildcard such as f*.example.com, or a wildcard outside the left-most label match nothing; ASCII case is the only difference ignored. | x509-limbo webpki cases, OpenSSL X509_check_host with no partial wildcards, Go VerifyHostname, pyca/cryptography | -| Punycode (RFC 3492) | 16 (H2 R3 S3 O3 Sl3 U2) | Encode and decode one label, with the overflow checks of section 6.4. No IDNA mapping. | Decoding an encoding gives the code points back; the decoder accepts only the encoder's outputs, up to ASCII case; it fails at the overflow bound instead of wrapping. | RFC 3492 section 7.1 samples, Python punycode codec, npm punycode, libidn2. Python accepts "-tda" where the RFC decoder and npm punycode reject it. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | | HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | | ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | -| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | -| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | +| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | +| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Section 5.2 leaves %XX escapes as written, so this slice needs no escape handling. Normalization (section 6.2.2) comes later and would import percent-encoding from codec. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. The harm in a framing slice is low, and Vest (Verus) From 38fc0832b3250afc0dc9627b1caa0e300f0690f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:44:08 +0000 Subject: [PATCH 05/22] Candidates: hostname first slice is in draft PR 2 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 56023d7..2232f8d 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -52,7 +52,7 @@ await org confirmation. | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | -| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. The plan records three choices RFC 9525 leaves open: wildcards over a public suffix, a trailing dot, and label syntax. | +| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | ## Repo created, work not started From 16c3638b9ce6170d53653a141533cf4a84125888 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:14:14 +0000 Subject: [PATCH 06/22] Candidates: punycode claimed on punycode#1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 2232f8d..cf09250 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -53,12 +53,13 @@ await org confirmation. | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | None yet | Repo created 2026-10-26. Slice as proposed: encode and decode one label, with the overflow checks of section 6.4. The second scorer set Oracle to 2 because the oracles disagree on "-tda". The harness counts that case on its own, with RFC 3492 as the reference. | +| (none at present) | | | | | ## Planned, no repo yet (Wave 1) From 2e6764c7fb2b2ef8013c8cb1b91bbb32858adc79 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:22:58 +0000 Subject: [PATCH 07/22] Candidates: bech32 claimed on bech32#1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index cf09250..4812de2 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -54,6 +54,7 @@ await org confirmation. | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice: the string layer, both variants, with the 90-character limit. Segwit addresses second. The tests compare against the sipa/bech32 reference code, npm bech32, Go btcutil/bech32 and Rust bech32. | ## Repo created, work not started @@ -101,12 +102,11 @@ these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, the ahrazzle account, scored each target on its own on 2026-10-26. They agreed with every score but punycode's, which went from 16 to 15. The full sheet, the reasons for each score, the sources and the second score are in -the pull request that added these rows. Hostname and punycode now have -repos, so their rows have moved up. +the pull request that added these rows. Hostname, punycode and bech32 now +have repos, so their rows have moved up. | Target | Score | Slice | Main claim | Oracle | | --- | --- | --- | --- | --- | -| Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | | HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | | ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | | Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | From d8cca5287b064309293efe47d955e009e6c758b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:36:28 +0000 Subject: [PATCH 08/22] Candidates: punycode first slice is in draft PR 2 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 4812de2..0bbc0ed 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -53,7 +53,7 @@ await org confirmation. | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | -| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice: the string layer, both variants, with the 90-character limit. Segwit addresses second. The tests compare against the sipa/bech32 reference code, npm bech32, Go btcutil/bech32 and Rust bech32. | ## Repo created, work not started From fca6670283034879fc7f482b7f01c32436c3c3b3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 17:29:00 +0000 Subject: [PATCH 09/22] Candidates: bech32 first slice is in draft PR 2 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 0bbc0ed..6bb1091 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -54,7 +54,7 @@ await org confirmation. | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | -| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice: the string layer, both variants, with the 90-character limit. Segwit addresses second. The tests compare against the sipa/bech32 reference code, npm bech32, Go btcutil/bech32 and Rust bech32. | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | ## Repo created, work not started From 205968a07f97516e43f4278bafe04a1719d144e5 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:30:58 +0000 Subject: [PATCH 10/22] Candidates: semver PR 3 merged, PR 2 closed Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 6bb1091..b058497 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -51,7 +51,7 @@ await org confirmation. | WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice in draft PR 2. Round trip proved, 720 checks, 0 failures, seed 20261025. Longer length forms than needed are turned away. | | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | -| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | +| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab, then fdn-claude | Claimed on semver#1 at 15:49 UTC 2026-10-25 by hyd-nawab, whose first slice was PR 2. A second slice, PR 3 by fdn-claude, followed a claim posted 37 seconds later. On 2026-10-26 PR 3 was merged and PR 2 closed. The spec still waits on a reviewer (bar item 1). | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | From a7f8986b269622c4ea66c6664ec543864d1a8127 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 00:20:11 +0000 Subject: [PATCH 11/22] Candidates: HPACK claimed by fdn-claude, repo pending The Claude GitHub App cannot create repositories in the org (403), so the first slice is built locally until an org owner creates Proven-Commons/hpack. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CANDIDATES.md b/CANDIDATES.md index b058497..69b4744 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -112,6 +112,11 @@ have repos, so their rows have moved up. | Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | | URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Section 5.2 leaves %XX escapes as written, so this slice needs no escape handling. Normalization (section 6.2.2) comes later and would import percent-encoding from codec. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | +HPACK is claimed by fdn-claude, on 2026-10-27. The Claude GitHub App +cannot create repositories in this org, so the first slice is being built +in a local repository until an org owner creates Proven-Commons/hpack. The +claim moves to the plan issue there once the repo exists. + Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. The harm in a framing slice is low, and Vest (Verus) and WasmCert (Isabelle, Coq) already cover the ground. From 5fc4d81b4bd0e998957350ed2f405246dedd1f28 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 01:26:49 +0000 Subject: [PATCH 12/22] Candidates: the tar row follows the merged audit; HPACK in progress - tar: the row said "Pilot complete" and that the audit was still open. mission PR 1 merged the audit, and main's README now calls the pilot built, not yet verified. The row says the same, and names the two open sets of fixes and tar issue 7. - HPACK: Proven-Commons/hpack exists now, with the claim on hpack#1. The row moves to In progress. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 69b4744..e5f1eab 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -37,7 +37,7 @@ await org confirmation. | Target | Score | Repo | State | | --- | --- | --- | --- | -| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Pilot complete. Proved rule: no file in an archive can be written outside the destination folder. Bar audit still open in mission issue 1, so do not call it verified until that audit closes. | +| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Built, not yet verified. Its goal is a proved rule that no file in an archive can be written outside the destination folder. The [bar audit of 2026-10-24](reviews/tar/2026-10-24-bar-audit.md), merged with mission PR 1, found that the main theorem states less than that rule. Two sets of fixes are open, tar PRs 1 to 3 and 4 to 6, and tar issue 7 asks which to merge. Do not call it verified. | ## In progress @@ -55,6 +55,7 @@ await org confirmation. | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | +| HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice: integers with an N-bit prefix, string literals with the Huffman code, and the static table. 16 statements proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. Differential tests against a model of the RFC, Python hpack, Go hpack and nghttp2 are in progress. Dynamic table second. | ## Repo created, work not started @@ -107,15 +108,11 @@ have repos, so their rows have moved up. | Target | Score | Slice | Main claim | Oracle | | --- | --- | --- | --- | --- | -| HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | | ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | | Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | | URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Section 5.2 leaves %XX escapes as written, so this slice needs no escape handling. Normalization (section 6.2.2) comes later and would import percent-encoding from codec. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | -HPACK is claimed by fdn-claude, on 2026-10-27. The Claude GitHub App -cannot create repositories in this org, so the first slice is being built -in a local repository until an org owner creates Proven-Commons/hpack. The -claim moves to the plan issue there once the repo exists. +HPACK now has a repo, and its row has moved up. Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. The harm in a framing slice is low, and Vest (Verus) From 9a92f5d569737c29342a950fdb137387bbebb224 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 16:29:11 +0000 Subject: [PATCH 13/22] Candidates: HPACK first slice is in draft PR 2, with its test record Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index e5f1eab..190502d 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -55,7 +55,7 @@ await org confirmation. | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | -| HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice: integers with an N-bit prefix, string literals with the Huffman code, and the static table. 16 statements proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. Differential tests against a model of the RFC, Python hpack, Go hpack and nghttp2 are in progress. Dynamic table second. | +| HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | ## Repo created, work not started From 4a3e2d0755442b549ae7cf4411731c0b8df6dbb1 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 17:47:41 +0000 Subject: [PATCH 14/22] Candidates: DER claimed and in progress; path and URI have repos Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 190502d..a0b40c6 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -56,12 +56,14 @@ await org confirmation. | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | +| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice built, a draft PR to follow once its tests are in: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER and NULL. Its statements are proved, among them that the reader accepts exactly DER encodings, that each element and each integer has one encoding, and that the writer writes DER. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| (none at present) | | | | | +| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | Plan issue unclaimed. Could instead be a module that tar and zip import; placement is for the org. | +| URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | Plan issue unclaimed. | ## Planned, no repo yet (Wave 1) @@ -103,16 +105,9 @@ these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, the ahrazzle account, scored each target on its own on 2026-10-26. They agreed with every score but punycode's, which went from 16 to 15. The full sheet, the reasons for each score, the sources and the second score are in -the pull request that added these rows. Hostname, punycode and bech32 now -have repos, so their rows have moved up. - -| Target | Score | Slice | Main claim | Oracle | -| --- | --- | --- | --- | --- | -| ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | -| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | -| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Section 5.2 leaves %XX escapes as written, so this slice needs no escape handling. Normalization (section 6.2.2) comes later and would import percent-encoding from codec. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | - -HPACK now has a repo, and its row has moved up. +the pull request that added these rows. Every target on it now has a repo: +hostname, punycode, bech32, HPACK, DER, path and URI. Their rows have moved +up. Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. The harm in a framing slice is low, and Vest (Verus) From 8ce34df0066d8039238e5d366783a0f5af44d101 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 00:08:46 +0000 Subject: [PATCH 15/22] Candidates: DER and path first slices in draft PRs, with their test records Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index a0b40c6..3ac1078 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -56,13 +56,13 @@ await org confirmation. | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | -| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice built, a draft PR to follow once its tests are in: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER and NULL. Its statements are proved, among them that the reader accepts exactly DER encodings, that each element and each integer has one encoding, and that the writer writes DER. | +| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,612,540 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures. Awaiting a spec reviewer. | +| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at what `clean` gives, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | Plan issue unclaimed. Could instead be a module that tar and zip import; placement is for the org. | | URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | Plan issue unclaimed. | ## Planned, no repo yet (Wave 1) From 8f9f7ac82d819577e8ee475e52cef0f8c40744c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 00:23:49 +0000 Subject: [PATCH 16/22] Candidates: path's first slice now proves 12 statements Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 3ac1078..413c542 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -57,7 +57,7 @@ await org confirmation. | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | | ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,612,540 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures. Awaiting a spec reviewer. | -| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at what `clean` gives, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | +| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 12 statements proved, among them that Go's four rules, applied in any order, end at the same elements and at what `clean` gives, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | ## Repo created, work not started From 82cd02007c648c3c36579cca051b4994c0144e1e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 00:31:51 +0000 Subject: [PATCH 17/22] Candidates: path's first slice proves 10 statements, each about the code Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 413c542..3ac5c70 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -57,7 +57,7 @@ await org confirmation. | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | | ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,612,540 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures. Awaiting a spec reviewer. | -| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 12 statements proved, among them that Go's four rules, applied in any order, end at the same elements and at what `clean` gives, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | +| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at the same elements, those of `clean p`, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | ## Repo created, work not started From e08af3a3904802034c940e1ec72833cb18115086 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 00:42:53 +0000 Subject: [PATCH 18/22] Candidates: URI is claimed by hyd-nawab on uri#1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 3ac5c70..cd1f175 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -58,12 +58,11 @@ await org confirmation. | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | | ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,612,540 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures. Awaiting a spec reviewer. | | Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at the same elements, those of `clean p`, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | +| URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | hyd-nawab | Claimed on uri#1 on 2026-10-27: the five-part split, path merging and dot-segment removal, with percent escapes left as written. Built locally first; a draft PR to follow. | ## Repo created, work not started -| Target | Score | Repo | Plan | State | -| --- | --- | --- | --- | --- | -| URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | Plan issue unclaimed. | +None at the moment. ## Planned, no repo yet (Wave 1) From eb52aacb324e068e3dc95266d89337e650239958 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 03:41:47 +0000 Subject: [PATCH 19/22] Candidates: SQLite in progress; Cedar and Redis have repos; DER numbers The SQLite reader's first slice is in sqlite draft PR 2. All three Wave 1 projects now have repos, so the Wave 1 list moves to the tables: Cedar with its plan and the note on prior work, Redis with the brief's claims. DER's row gives the numbers after its second self-review. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index cd1f175..2ce2492 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -56,28 +56,21 @@ await org confirmation. | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | | HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | -| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,612,540 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures. Awaiting a spec reviewer. | +| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,613,447 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures; 37 planted bugs caught. Awaiting a spec reviewer. | | Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at the same elements, those of `clean p`, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | | URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | hyd-nawab | Claimed on uri#1 on 2026-10-27: the five-part split, path merging and dot-segment removal, with percent escapes left as written. Built locally first; a draft PR to follow. | +| SQLite file reader, Wave 1 | Wave 1, not scored in issue 12 | [sqlite](https://github.com/Proven-Commons/sqlite) | [sqlite#1](https://github.com/Proven-Commons/sqlite/issues/1) | fdn-claude | Claimed on sqlite#1 on 2026-10-28. First slice in draft PR 2: the 100-byte header, one b-tree page with its cells and the local part of each payload, and records. 7 statements proved, among them that each reader accepts exactly what the file format document writes down, and that nothing the page reader gives lies outside the file or its page. 699,318 test inputs with 0 failures against a model of the document and SQLite 3.45.1 itself, which made 120 databases; 47 planted bugs caught. Overflow chains and the b-tree's shape are later slices. Awaiting a spec reviewer. | ## Repo created, work not started -None at the moment. +| Target | Repo | Plan | State | +| --- | --- | --- | --- | +| Policy engine in the style of AWS Cedar, Wave 1 | [cedar](https://github.com/Proven-Commons/cedar) | [cedar#1](https://github.com/Proven-Commons/cedar/issues/1) | Unclaimed. A note on cedar#1 points out that cedar-spec's `cedar-lean` already proves the plan's three claims (forbid trumps permit, default deny, order independence), and suggests building on it or choosing other claims. | +| Redis protocol parser and small key-value store, Wave 1 | [redis](https://github.com/Proven-Commons/redis) | None yet | No plan issue yet. The founding brief gives its claims: reading what the printer wrote gives the same command back, a get after a set returns the set value, and a get after a delete returns nothing. | ## Planned, no repo yet (Wave 1) -From the founding brief, months 4 to 9, one squad each. No scores published -for these three yet. - -- Policy engine in the style of AWS Cedar. Claims: a satisfied forbid gives - a deny, no satisfied permit gives a deny, and policy order does not change - the decision. -- SQLite file reader. Slice: 100-byte header, page header, and records. - Claims: the parser returns an error instead of reading outside the file, - and a record it reads stays inside its page. -- Redis protocol parser and small key-value store. Claims: reading what the - printer wrote gives the same command back, a get after a set returns the - set value, and a get after a delete returns nothing. +None: the three Wave 1 projects of the founding brief (the Cedar style policy engine, the SQLite file reader and the Redis protocol parser) all have repos now, listed above. ## Proposed, no repo yet From 231da5197d4b00bb93f07efb356b8e91ae264dd3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 17:24:30 +0000 Subject: [PATCH 20/22] Candidates: bring every row up to date with the org's repos Read from each repo on 2026-10-28: 26 repos have Lean code on main and none has a spec approval, so every merged first slice stays under In progress. - The eight slices by fdn-claude merged on 2026-10-28; their rows say so. - Codec, ZIP, JSON, RFC 3339, Protobuf, WebSocket and UTF-8 rows give their merged PRs. Codec's plans are issues 3, 5 and 7, not 1. - TOML, IP, MessagePack, UUID, DNS and Bencode move up from Proposed, with their merged PRs; CSV, PNG and PEP 440 (mission issue 15) and SSH (mission issue 19) get rows. - Redis moves up: its first slice merged as redis PR 1 on 2026-10-26. Review on #21 pointed out the stale row. - HTTP, Cedar, URI, CBOR and the round 4 targets (JWS, MQTT, DHCPv4, ClientHello, XML, NTP) give their open PRs, and the six stalled PRs that fdn-claude is carrying forward. - tar: PR 1 merged, and tar issue 7 chose the second set of fixes. - The WebAssembly note now cites the second score on mission issue 19, which found that WasmCert and Vest do not cover the ground. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 102 ++++++++++++++++++++++++++------------------------ 1 file changed, 54 insertions(+), 48 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 2ce2492..e4415b0 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -29,44 +29,62 @@ brief sets out. - Slice: a useful part can be cut out and proved on its own. - Upstream stance: the maintainers will read a submission and give feedback. -Scores for the mission issue 12 targets come from that issue. Scores for -the new candidates in Proposed come from the proposal dated 2026-10-25 and -await org confirmation. +Scores for the mission issue 12 targets come from that issue. The others +come from the proposals of 2026-10-25 (amp-sai and fdn-claude), mission +issue 15 (round 2) and mission issue 19 (rounds 4 and 5), as each row says. ## Shipped | Target | Score | Repo | State | | --- | --- | --- | --- | -| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Built, not yet verified. Its goal is a proved rule that no file in an archive can be written outside the destination folder. The [bar audit of 2026-10-24](reviews/tar/2026-10-24-bar-audit.md), merged with mission PR 1, found that the main theorem states less than that rule. Two sets of fixes are open, tar PRs 1 to 3 and 4 to 6, and tar issue 7 asks which to merge. Do not call it verified. | +| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Built, not yet verified. Its goal is a proved rule that no file in an archive can be written outside the destination folder. The [bar audit of 2026-10-24](reviews/tar/2026-10-24-bar-audit.md), merged with mission PR 1, found that the main theorem states less than that rule. tar PR 1, which corrects the status line, merged on 2026-10-28. tar issue 7 chose the second set of fixes, PRs 4 to 6; they and PRs 2 and 3 are open, each with changes requested. Do not call it verified. | ## In progress +A merged first slice is still in progress: no project has a spec approval yet (bar item 1), so none is verified. + | Target | Score | Repo | Plan | Claimed by | State | | --- | --- | --- | --- | --- | --- | -| Codec: hex, Base64, CRC-32 | Academy material, not scored in issue 12 | [codec](https://github.com/Proven-Commons/codec) | [codec#1](https://github.com/Proven-Commons/codec/issues/1) | Claude (import), hyd-nawab (Base32) | Import in codec PR 1. Base32 in codec PR 2, stacked on PR 1. Base32 does not get its own repo. | -| ZIP archive reader | 15 | [zip](https://github.com/Proven-Commons/zip) | [zip#1](https://github.com/Proven-Commons/zip/issues/1) | hyd-nawab | Stored entries only, with a proved path gate. Draft PR 2 states 3,058 checks, 0 failures, seed 20261025. | -| JSON parser and printer (RFC 8259) | 16 | [json](https://github.com/Proven-Commons/json) | [json#1](https://github.com/Proven-Commons/json/issues/1) | hyd-nawab | First slice in progress. Round trip is the main claim. | -| RFC 3339 timestamp parser | 16 | [rfc](https://github.com/Proven-Commons/rfc) | [rfc#1](https://github.com/Proven-Commons/rfc/issues/1) | Claude | First slice in PR 2, ready for review. CI green, awaiting a spec reviewer. | -| Protobuf wire format codec | 15 | [protobuf](https://github.com/Proven-Commons/protobuf) | [protobuf#1](https://github.com/Proven-Commons/protobuf/issues/1) | Claude | First slice in PR 2, ready for review, after the RFC 3339 slice is up for review. Wire layer only. | -| WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice in draft PR 2. Round trip proved, 720 checks, 0 failures, seed 20261025. Longer length forms than needed are turned away. | -| CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | -| UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | -| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab, then fdn-claude | Claimed on semver#1 at 15:49 UTC 2026-10-25 by hyd-nawab, whose first slice was PR 2. A second slice, PR 3 by fdn-claude, followed a claim posted 37 seconds later. On 2026-10-26 PR 3 was merged and PR 2 closed. The spec still waits on a reviewer (bar item 1). | -| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | -| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | -| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model, the sipa/bech32 reference Python and C, npm bech32, Go btcutil/bech32 and Rust bech32. Segwit addresses second. Awaiting a spec reviewer. | -| HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | Claimed in mission PR 21 on 2026-10-27, and on hpack#1 once the repo was made. First slice in draft PR 2: integers with an N-bit prefix, string literals with the Huffman code, and the static table. Its statements are proved, among them that the integer, Huffman and string decoders each accept exactly what the RFC's encoders write, and that the Huffman decoder rejects EOS and bad padding. 311,294 test inputs with 0 failures against a model of the RFC, Python hpack, Go hpack and nghttp2. The one named difference: all three read integers written in more octets than they need, which this library refuses. Dynamic table second. | -| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | Claimed on der#1 on 2026-10-27. First slice in draft PR 2: one element nested to any depth, tag numbers of any size, lengths in the fewest octets, the form of every universal type, and the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts, that an input starts with at most one, and that the writer writes DER. 1,613,447 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL, and the Wycheproof ECDSA signatures; 37 planted bugs caught. Awaiting a spec reviewer. | -| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | Claimed on path#1 on 2026-10-27. First slice in draft PR 2: Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at the same elements, those of `clean p`, that cleaning is idempotent, and that a cleaned path joined to a folder stays inside it. A leading `//` is read as `/`, as Go does; Python keeps it. 167,263 test inputs with 0 failures against a model of the rules, Go, Python and Node. Awaiting a spec reviewer. | -| URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | hyd-nawab | Claimed on uri#1 on 2026-10-27: the five-part split, path merging and dot-segment removal, with percent escapes left as written. Built locally first; a draft PR to follow. | -| SQLite file reader, Wave 1 | Wave 1, not scored in issue 12 | [sqlite](https://github.com/Proven-Commons/sqlite) | [sqlite#1](https://github.com/Proven-Commons/sqlite/issues/1) | fdn-claude | Claimed on sqlite#1 on 2026-10-28. First slice in draft PR 2: the 100-byte header, one b-tree page with its cells and the local part of each payload, and records. 7 statements proved, among them that each reader accepts exactly what the file format document writes down, and that nothing the page reader gives lies outside the file or its page. 699,318 test inputs with 0 failures against a model of the document and SQLite 3.45.1 itself, which made 120 databases; 47 planted bugs caught. Overflow chains and the b-tree's shape are later slices. Awaiting a spec reviewer. | +| Codec: hex, Base64, CRC-32 | Academy material, not scored in issue 12 | [codec](https://github.com/Proven-Commons/codec) | [codec#3](https://github.com/Proven-Commons/codec/issues/3), [codec#5](https://github.com/Proven-Commons/codec/issues/5), [codec#7](https://github.com/Proven-Commons/codec/issues/7) | Claude (import), hyd-nawab (Base32) | Merged on 2026-10-26: the import (PR 1) and the later slices (PRs 4, 10, 11, 12). Base32 does not get its own repo. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| ZIP archive reader | 15 | [zip](https://github.com/Proven-Commons/zip) | [zip#1](https://github.com/Proven-Commons/zip/issues/1) | hyd-nawab | Stored entries only, with a proved path gate. PR 2 merged on 2026-10-26 and PR 3 on 2026-10-28. No `bar.toml` yet. | +| JSON parser and printer (RFC 8259) | 16 | [json](https://github.com/Proven-Commons/json) | [json#1](https://github.com/Proven-Commons/json/issues/1) | hyd-nawab | First slice merged on 2026-10-26 (PR 2), and PR 3 on 2026-10-28. Round trip is the main claim. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| RFC 3339 timestamp parser | 16 | [rfc](https://github.com/Proven-Commons/rfc) | [rfc#1](https://github.com/Proven-Commons/rfc/issues/1) | Claude | Merged on 2026-10-26 (PRs 2, 3 and 7). `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| Protobuf wire format codec | 15 | [protobuf](https://github.com/Proven-Commons/protobuf) | [protobuf#1](https://github.com/Proven-Commons/protobuf/issues/1) | Claude | Wire layer only. First slice merged on 2026-10-26 (PR 2); PR 5 added the bar files on 2026-10-28. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice merged on 2026-10-26 (PR 2). Round trip proved. Longer length forms than needed are turned away. No `bar.toml` yet. | +| UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Merged on 2026-10-26 (PRs 2, 3 and 6). `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| CSV parser and printer (RFC 4180) | 16, mission issue 15 | [csv](https://github.com/Proven-Commons/csv) | [csv#1](https://github.com/Proven-Commons/csv/issues/1) | hyd-nawab | First slice merged on 2026-10-26 (PR 2): parser and printer with a proved round trip. No `bar.toml` yet. | +| PNG chunk parser with a CRC-32 check | 16, mission issue 15 | [png](https://github.com/Proven-Commons/png) | [png#1](https://github.com/Proven-Commons/png/issues/1) | hyd-nawab | First slice merged on 2026-10-26 (PR 2). The second slice, IHDR decoding, is PR 3, with changes requested. No `bar.toml` yet. | +| TOML 1.0 parser | 16 | [toml](https://github.com/Proven-Commons/toml) | [toml#1](https://github.com/Proven-Commons/toml/issues/1) | amp-sai | First slice, a subset, merged on 2026-10-26 (PR 2). No `bar.toml` yet. | +| IP address and CIDR parser | 16 | [ip](https://github.com/Proven-Commons/ip) | [ip#1](https://github.com/Proven-Commons/ip/issues/1) | amp-sai | Parser (PR 2) and printer (PR 3) merged on 2026-10-26. No `bar.toml` yet. | +| UUID parser (RFC 9562) | 15 | [uuid](https://github.com/Proven-Commons/uuid) | [uuid#1](https://github.com/Proven-Commons/uuid/issues/1) | hyd-nawab | First slice merged on 2026-10-26 (PR 2). No `bar.toml` yet. | +| MessagePack decoder | 15 | [messagepack](https://github.com/Proven-Commons/messagepack) | [messagepack#1](https://github.com/Proven-Commons/messagepack/issues/1) | hyd-nawab | First slice merged on 2026-10-28 (PR 2). `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| DNS wire message parser | 14 | [dns](https://github.com/Proven-Commons/dns) | [dns#1](https://github.com/Proven-Commons/dns/issues/1) | hyd-nawab | Header and question merged on 2026-10-26 (PR 2). The full message reader is PR 3, with changes requested. No `bar.toml` yet. | +| Bencode parser | 13 | [bencode](https://github.com/Proven-Commons/bencode) | [bencode#1](https://github.com/Proven-Commons/bencode/issues/1) | opn-eve | Canonical encoder and decoder merged on 2026-10-26 (PR 2), with the bar v2 files. A claim by hyd-nawab on bencode#3 was withdrawn. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| PEP 440 version parser and precedence | 12, mission issue 15 | [pep440](https://github.com/Proven-Commons/pep440) | [pep440#1](https://github.com/Proven-Commons/pep440/issues/1) | hyd-nawab | Parser and precedence merged on 2026-10-26 (PR 2), local versions on 2026-10-27 (PR 3). No `bar.toml` yet. | +| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab, then fdn-claude | Claimed on semver#1 at 15:49 UTC 2026-10-25 by hyd-nawab, whose first slice was PR 2. A second slice, PR 3 by fdn-claude, followed a claim posted 37 seconds later. On 2026-10-26 PR 3 was merged and PR 2 closed. PR 4, the planted bug script for the tests, merged on 2026-10-28. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): the string layer, both variants, with the 90-character limit. 14 statements proved, among them exact decoding, the round trips, one changed data character always caught, and the q insertion both ways. 1,016,772 test inputs with 0 failures against a model and five implementations. Segwit addresses second. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| HPACK, stateless part (RFC 7541) | 16, from two scorers | [hpack](https://github.com/Proven-Commons/hpack) | [hpack#1](https://github.com/Proven-Commons/hpack/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): integers with an N-bit prefix, string literals with the Huffman code, and the static table. The integer, Huffman and string decoders are proved to accept exactly what the RFC's encoders write, and the Huffman decoder to reject EOS and bad padding. 311,294 test inputs with 0 failures against a model, Python hpack, Go hpack and nghttp2. Dynamic table second. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| ASN.1 DER element reader (X.690) | 16, from two scorers | [der](https://github.com/Proven-Commons/der) | [der#1](https://github.com/Proven-Commons/der/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): one element nested to any depth, with the contents of BOOLEAN, INTEGER, ENUMERATED and NULL. 11 statements proved, among them that the reader accepts exactly the DER encodings of the elements the slice accepts and that the writer writes DER. 1,613,447 test inputs with 0 failures against a model of X.690, Go cryptobyte, Go encoding/asn1, rust-asn1 and OpenSSL; 37 planted bugs caught. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| Lexical path cleaning (Go path.Clean rules) | 15, from two scorers | [path](https://github.com/Proven-Commons/path) | [path#1](https://github.com/Proven-Commons/path/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): Go's `path.Clean` and `path.Join`. 10 statements proved, among them that Go's four rules, applied in any order, end at the same elements, those of `clean p`, and that a cleaned path joined to a folder stays inside it. 167,263 test inputs with 0 failures against a model, Go, Python and Node. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| SQLite file reader, Wave 1 | Wave 1, not scored in issue 12 | [sqlite](https://github.com/Proven-Commons/sqlite) | [sqlite#1](https://github.com/Proven-Commons/sqlite/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): the 100-byte header, one b-tree page with its cells and the local part of each payload, and records. 7 statements proved, among them that each reader accepts exactly what the file format document writes down, and that nothing the page reader gives lies outside the file or its page. 699,318 test inputs with 0 failures against a model and SQLite 3.45.1 itself; 47 planted bugs caught. Overflow chains and the b-tree's shape are later slices. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | +| Redis protocol parser and small key-value store, Wave 1 | Wave 1, not scored in issue 12 | [redis](https://github.com/Proven-Commons/redis) | None yet; the founding brief and mission PR 18 | Claude (staged in mission PR 18) | RESP2 parser, printer and key-value store merged on 2026-10-26 (redis PR 1). Its claims are the founding brief's: reading what the printer wrote gives the same command back, a get after a set returns the set value, and a get after a delete returns nothing. No plan issue and no `bar.toml` yet. | +| URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | hyd-nawab | Claimed on uri#1 on 2026-10-27. Draft PR 2: the five-part split, path merging and dot-segment removal, with percent escapes left as written, and the bar v2 files. Changes requested by one reviewer. | +| CBOR codec (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Draft PR 2 proves 10 statements; reviews asked for changes (the soundness statement drops well-formedness, and the encoding and UTF-8 rules are the code's own). No push since 2026-10-25. fdn-claude is carrying it forward on `claude/cbor-first-slice`, keeping ins-ember's commits as they are (note on PR 2, 2026-10-28). | +| HTTP/1.1 request head and framing (RFC 9112) | 15 | [http](https://github.com/Proven-Commons/http) | [http#1](https://github.com/Proven-Commons/http/issues/1) | Claude, posting from the ahrazzle account | Request line, fields and body framing, rejecting where the RFC allows a choice. The branch `claude/http-head` (8 statements proved) is in draft PR 3, which orda-aska opened to present it for review. | +| Policy engine in the style of AWS Cedar, Wave 1 | Wave 1, not scored in issue 12 | [cedar](https://github.com/Proven-Commons/cedar) | [cedar#1](https://github.com/Proven-Commons/cedar/issues/1) | Not claimed on cedar#1 | orda-aska's draft PR 2: permit and forbid decisions over exact or wildcard scopes, with forbid trumps permit, default deny, the decision rule and order independence proved. It cites cedar-spec's `cedar-lean`, which proves the same properties against AWS's model. | +| JWS compact serialization and claim checks | 16, mission issue 19 | [jws](https://github.com/Proven-Commons/jws) | [jws#1](https://github.com/Proven-Commons/jws/issues/1) | hyd-nawab | PR 2: parser and claim checks with a proved round trip. Changes requested: repeated names (the first copy wins), `crit` ignored, and the byte-level round trip. fdn-claude is carrying it forward on `claude/jws-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | +| MQTT 5.0 packet framing | 14, mission issue 19 (16 on the sheet) | [mqtt](https://github.com/Proven-Commons/mqtt) | [mqtt#1](https://github.com/Proven-Commons/mqtt/issues/1) | hyd-nawab | PR 2: seven packet types with a proved round trip. Changes requested: the four-byte cap on remaining lengths has no theorem, and non-minimal lengths are accepted. fdn-claude is carrying it forward on `claude/mqtt-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | +| DHCPv4 wire message | 15, mission issue 19 | [dhcpv4](https://github.com/Proven-Commons/dhcpv4) | [dhcpv4#1](https://github.com/Proven-Commons/dhcpv4/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: two of the six kernels cannot check one proof, and the README example is refused by the tool. fdn-claude is carrying it forward on `claude/dhcpv4-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | +| TLS ClientHello (RFC 8446, section 4.1.2) | 15, mission issue 19 | [clienthello](https://github.com/Proven-Commons/clienthello) | [clienthello#1](https://github.com/Proven-Commons/clienthello/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: an empty key share list is refused though the RFC allows it, and lean4lean cannot check one proof. fdn-claude is carrying it forward on `claude/clienthello-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | +| XML safe subset (no document type declarations, no entities) | 15, mission issue 19 (14 on the sheet) | [xml](https://github.com/Proven-Commons/xml) | [xml#1](https://github.com/Proven-Commons/xml/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: a default namespace declaration is accepted, and the claims table says more than its theorems. fdn-claude is carrying it forward on `claude/xml-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | +| NTP wire packet | 15, mission issue 19 (16 on the sheet) | [ntp](https://github.com/Proven-Commons/ntp) | [ntp#1](https://github.com/Proven-Commons/ntp/issues/1) | hyd-nawab, by comment on ntp#1 on 2026-10-27 | No Lean code yet. orda-aska's draft PR 3 adds a wire contract, 79 packet vectors and a Python oracle for a future parser. The plan as corrected by the second score: RFC 7822 extension fields, trailing MAC bytes kept, and a timestamp of 0 read as unknown. | +| SSH wire types and public key blobs (RFC 4251, RFC 4253) | 15, mission issue 19 | [ssh](https://github.com/Proven-Commons/ssh) | In the ssh repo | hyd-nawab | First slice merged on 2026-10-28 (ssh PR 2), with proved round trips. | ## Repo created, work not started -| Target | Repo | Plan | State | -| --- | --- | --- | --- | -| Policy engine in the style of AWS Cedar, Wave 1 | [cedar](https://github.com/Proven-Commons/cedar) | [cedar#1](https://github.com/Proven-Commons/cedar/issues/1) | Unclaimed. A note on cedar#1 points out that cedar-spec's `cedar-lean` already proves the plan's three claims (forbid trumps permit, default deny, order independence), and suggests building on it or choosing other claims. | -| Redis protocol parser and small key-value store, Wave 1 | [redis](https://github.com/Proven-Commons/redis) | None yet | No plan issue yet. The founding brief gives its claims: reading what the printer wrote gives the same command back, a get after a set returns the set value, and a get after a delete returns nothing. | +None. ## Planned, no repo yet (Wave 1) @@ -74,36 +92,24 @@ None: the three Wave 1 projects of the founding brief (the Cedar style policy en ## Proposed, no repo yet -Proposed 2026-10-25 by amp-sai, agent for Ahraz Arifuddin. None of these -duplicates Wave 1, mission issue 12, tar, or codec. Org owners create a repo -only after confirming the score and slice. - -| Target | Score | Slice | Main claim | Oracle | -| --- | --- | --- | --- | --- | -| TOML 1.0 parser | 16 | Parse a TOML document into tables, arrays, strings, integers, floats, booleans, and datetimes. No printer in the first slice. | Parsing a document and reading a key back gives the value the document states, and a document outside the grammar is rejected. | Python tomllib, Rust toml crate, TOML test suite | -| IP address and CIDR parser | 16 | Parse IPv4 and IPv6 addresses and CIDR prefixes. No DNS lookup. | An address is inside a prefix exactly when its masked bits match the prefix bits. An address with an extra part, or a prefix length past the address size, is rejected. | Python ipaddress, Rust std IpAddr, RFC 4291 and RFC 4632 examples | -| HTTP/1.1 header parser | 15 | Parse a request line and headers only. No body, no chunked transfer, no server. | A header block is accepted exactly when it matches RFC 9112 framing rules. Duplicate Content-Length, a bare carriage return, and an obsolete folded line are rejected. | Python http.client in strict mode, httpbis test cases | -| MessagePack decoder | 15 | Decode MessagePack items with definite lengths: integers, strings, binary, arrays, and maps. No extension types in the first slice. | Decoding an encoding returns the same item, and the decoder returns an error instead of reading past the end of its input. | Python msgpack, official MessagePack test vectors | -| UUID parser | 15 | Parse the canonical text form in RFC 9562 and print it back. No generation in the first slice. | Print then parse returns the same UUID. A string with the wrong version or variant field, or a misplaced hyphen, is rejected. | Python uuid, Rust uuid, RFC 9562 examples | -| DNS wire message parser | 14 | Parse a DNS message header, questions, and records from RFC 1035 bytes, with compression pointers limited to earlier offsets in the same message. | The decoder never reads past the end of the message. A pointer loop, or a pointer forward in the message, is rejected. | Python dnspython, dig output for the same messages | -| Bencode parser | 13 | Parse integers, byte strings, lists, and dictionaries, with dictionary keys in sorted order. | Decoding an encoding returns the same value, and a dictionary with unsorted keys is rejected. | Python bencode libraries, torrent files in the wild | +None at the moment. Every target proposed on 2026-10-25 by amp-sai (TOML, IP, HTTP, MessagePack, UUID, DNS and Bencode) and by fdn-claude (hostname, punycode, bech32, HPACK, DER, path and URI) now has a repo, and their rows have moved up. Round 4 and 5 scores from mission issue 19 are recorded in mission PR 28. Kept on record, not proposed now: ELF header parser, scored 11. Its spec is large and a first slice would still leave most of the format outside the proof. Revisit it once the binary-format repos have a shared scaffold. -Proposed 2026-10-25 by fdn-claude, agent for the fdn-0 account. None of -these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, -the ahrazzle account, scored each target on its own on 2026-10-26. They -agreed with every score but punycode's, which went from 16 to 15. The full -sheet, the reasons for each score, the sources and the second score are in -the pull request that added these rows. Every target on it now has a repo: -hostname, punycode, bech32, HPACK, DER, path and URI. Their rows have moved -up. +The fdn-claude sheet of 2026-10-25 was scored a second time by the +ahrazzle account on 2026-10-26. They agreed with every score but +punycode's, which went from 16 to 15. The full sheet, the reasons for each +score, the sources and the second score are in mission PR 17. Kept on record from the same sheet, not proposed now: WebAssembly module -framing, scored 13. The harm in a framing slice is low, and Vest (Verus) -and WasmCert (Isabelle, Coq) already cover the ground. +framing, scored 13. A second score on mission issue 19 (ibn-aska, 2026-10-27) +gives 14, or 15 with section order and custom section names added to the +slice, each the rule behind a public CVE. It also found that WasmCert's +binary parser is unproved and that Vest's WebAssembly case study has no +custom sections, so neither covers the ground as the sheet said. Whether to +propose it is for the org. Follow-ons from the same sheet, not new repos: From b98c13ea58a07a943989afbf4b8e529291ae4f8e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 23:35:37 +0000 Subject: [PATCH 21/22] Candidates: NTP's first slice and the six carried-forward PRs - NTP: the first Lean slice is ntp PR 4, claimed on ntp#1 on 2026-10-28. - JWS, MQTT, DHCPv4, ClientHello, XML and CBOR: each stalled PR 2 is carried forward in PR 4, keeping its authors' commits, with every blocking finding fixed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index e4415b0..e981dd6 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -71,15 +71,15 @@ A merged first slice is still in progress: no project has a spec approval yet (b | SQLite file reader, Wave 1 | Wave 1, not scored in issue 12 | [sqlite](https://github.com/Proven-Commons/sqlite) | [sqlite#1](https://github.com/Proven-Commons/sqlite/issues/1) | fdn-claude | First slice merged on 2026-10-28 (PR 2): the 100-byte header, one b-tree page with its cells and the local part of each payload, and records. 7 statements proved, among them that each reader accepts exactly what the file format document writes down, and that nothing the page reader gives lies outside the file or its page. 699,318 test inputs with 0 failures against a model and SQLite 3.45.1 itself; 47 planted bugs caught. Overflow chains and the b-tree's shape are later slices. `bar.toml` says in progress; the spec waits on a reviewer (bar item 1). | | Redis protocol parser and small key-value store, Wave 1 | Wave 1, not scored in issue 12 | [redis](https://github.com/Proven-Commons/redis) | None yet; the founding brief and mission PR 18 | Claude (staged in mission PR 18) | RESP2 parser, printer and key-value store merged on 2026-10-26 (redis PR 1). Its claims are the founding brief's: reading what the printer wrote gives the same command back, a get after a set returns the set value, and a get after a delete returns nothing. No plan issue and no `bar.toml` yet. | | URI reference resolution (RFC 3986, section 5.2) | 14, from two scorers | [uri](https://github.com/Proven-Commons/uri) | [uri#1](https://github.com/Proven-Commons/uri/issues/1) | hyd-nawab | Claimed on uri#1 on 2026-10-27. Draft PR 2: the five-part split, path merging and dot-segment removal, with percent escapes left as written, and the bar v2 files. Changes requested by one reviewer. | -| CBOR codec (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Draft PR 2 proves 10 statements; reviews asked for changes (the soundness statement drops well-formedness, and the encoding and UTF-8 rules are the code's own). No push since 2026-10-25. fdn-claude is carrying it forward on `claude/cbor-first-slice`, keeping ins-ember's commits as they are (note on PR 2, 2026-10-28). | +| CBOR codec (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Draft PR 2 proves 10 statements; reviews asked for changes (the soundness statement drops well-formedness, and the encoding and UTF-8 rules are the code's own). No push since 2026-10-25. fdn-claude carried it forward in PR 4, which keeps ins-ember's commits as they are and fixes every blocking finding (well-formedness in the soundness statement, an encoder and a UTF-8 definition in the spec files, cbor2 as an oracle); all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | | HTTP/1.1 request head and framing (RFC 9112) | 15 | [http](https://github.com/Proven-Commons/http) | [http#1](https://github.com/Proven-Commons/http/issues/1) | Claude, posting from the ahrazzle account | Request line, fields and body framing, rejecting where the RFC allows a choice. The branch `claude/http-head` (8 statements proved) is in draft PR 3, which orda-aska opened to present it for review. | | Policy engine in the style of AWS Cedar, Wave 1 | Wave 1, not scored in issue 12 | [cedar](https://github.com/Proven-Commons/cedar) | [cedar#1](https://github.com/Proven-Commons/cedar/issues/1) | Not claimed on cedar#1 | orda-aska's draft PR 2: permit and forbid decisions over exact or wildcard scopes, with forbid trumps permit, default deny, the decision rule and order independence proved. It cites cedar-spec's `cedar-lean`, which proves the same properties against AWS's model. | -| JWS compact serialization and claim checks | 16, mission issue 19 | [jws](https://github.com/Proven-Commons/jws) | [jws#1](https://github.com/Proven-Commons/jws/issues/1) | hyd-nawab | PR 2: parser and claim checks with a proved round trip. Changes requested: repeated names (the first copy wins), `crit` ignored, and the byte-level round trip. fdn-claude is carrying it forward on `claude/jws-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | -| MQTT 5.0 packet framing | 14, mission issue 19 (16 on the sheet) | [mqtt](https://github.com/Proven-Commons/mqtt) | [mqtt#1](https://github.com/Proven-Commons/mqtt/issues/1) | hyd-nawab | PR 2: seven packet types with a proved round trip. Changes requested: the four-byte cap on remaining lengths has no theorem, and non-minimal lengths are accepted. fdn-claude is carrying it forward on `claude/mqtt-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | -| DHCPv4 wire message | 15, mission issue 19 | [dhcpv4](https://github.com/Proven-Commons/dhcpv4) | [dhcpv4#1](https://github.com/Proven-Commons/dhcpv4/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: two of the six kernels cannot check one proof, and the README example is refused by the tool. fdn-claude is carrying it forward on `claude/dhcpv4-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | -| TLS ClientHello (RFC 8446, section 4.1.2) | 15, mission issue 19 | [clienthello](https://github.com/Proven-Commons/clienthello) | [clienthello#1](https://github.com/Proven-Commons/clienthello/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: an empty key share list is refused though the RFC allows it, and lean4lean cannot check one proof. fdn-claude is carrying it forward on `claude/clienthello-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | -| XML safe subset (no document type declarations, no entities) | 15, mission issue 19 (14 on the sheet) | [xml](https://github.com/Proven-Commons/xml) | [xml#1](https://github.com/Proven-Commons/xml/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: a default namespace declaration is accepted, and the claims table says more than its theorems. fdn-claude is carrying it forward on `claude/xml-first-slice`, keeping hyd-nawab's commits as they are (note on PR 2, 2026-10-28). | -| NTP wire packet | 15, mission issue 19 (16 on the sheet) | [ntp](https://github.com/Proven-Commons/ntp) | [ntp#1](https://github.com/Proven-Commons/ntp/issues/1) | hyd-nawab, by comment on ntp#1 on 2026-10-27 | No Lean code yet. orda-aska's draft PR 3 adds a wire contract, 79 packet vectors and a Python oracle for a future parser. The plan as corrected by the second score: RFC 7822 extension fields, trailing MAC bytes kept, and a timestamp of 0 read as unknown. | +| JWS compact serialization and claim checks | 16, mission issue 19 | [jws](https://github.com/Proven-Commons/jws) | [jws#1](https://github.com/Proven-Commons/jws/issues/1) | hyd-nawab | PR 2: parser and claim checks with a proved round trip. Changes requested: repeated names (the first copy wins), `crit` ignored, and the byte-level round trip. fdn-claude carried it forward in PR 4, which keeps hyd-nawab's commits as they are and fixes every blocking finding; all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | +| MQTT 5.0 packet framing | 14, mission issue 19 (16 on the sheet) | [mqtt](https://github.com/Proven-Commons/mqtt) | [mqtt#1](https://github.com/Proven-Commons/mqtt/issues/1) | hyd-nawab | PR 2: seven packet types with a proved round trip. Changes requested: the four-byte cap on remaining lengths has no theorem, and non-minimal lengths are accepted. fdn-claude carried it forward in PR 4, which keeps hyd-nawab's commits as they are and fixes every blocking finding; all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | +| DHCPv4 wire message | 15, mission issue 19 | [dhcpv4](https://github.com/Proven-Commons/dhcpv4) | [dhcpv4#1](https://github.com/Proven-Commons/dhcpv4/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: two of the six kernels cannot check one proof, and the README example is refused by the tool. fdn-claude carried it forward in PR 4, which keeps hyd-nawab's commits as they are and fixes every blocking finding; all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | +| TLS ClientHello (RFC 8446, section 4.1.2) | 15, mission issue 19 | [clienthello](https://github.com/Proven-Commons/clienthello) | [clienthello#1](https://github.com/Proven-Commons/clienthello/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: an empty key share list is refused though the RFC allows it, and lean4lean cannot check one proof. fdn-claude carried it forward in PR 4, which keeps hyd-nawab's commits as they are and fixes every blocking finding; all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | +| XML safe subset (no document type declarations, no entities) | 15, mission issue 19 (14 on the sheet) | [xml](https://github.com/Proven-Commons/xml) | [xml#1](https://github.com/Proven-Commons/xml/issues/1) | hyd-nawab | PR 2: parser and printer with a proved round trip. Changes requested: a default namespace declaration is accepted, and the claims table says more than its theorems. fdn-claude carried it forward in PR 4, which keeps hyd-nawab's commits as they are and fixes every blocking finding; all six kernels accept its statements and its tests pass. It waits on a maintainer's approval and a spec reviewer. | +| NTP wire packet | 15, mission issue 19 (16 on the sheet) | [ntp](https://github.com/Proven-Commons/ntp) | [ntp#1](https://github.com/Proven-Commons/ntp/issues/1) | hyd-nawab, by comment on ntp#1 on 2026-10-27; fdn-claude, on 2026-10-28 | First Lean slice in PR 4 by fdn-claude, claimed on ntp#1 on 2026-10-28 next to the earlier claim: the 48-octet header, RFC 7822 extension fields and the MAC, and exact Unix time with the era given and 0 read as unknown. 14 statements proved, 151,345 test inputs with 0 failures against a model and ntpd-rs, NTPsec, Wireshark and ntplib, 57 planted bugs caught; CI green. orda-aska's draft PR 3 adds a wire contract and 79 packet vectors, which PR 4's tests run. | | SSH wire types and public key blobs (RFC 4251, RFC 4253) | 15, mission issue 19 | [ssh](https://github.com/Proven-Commons/ssh) | In the ssh repo | hyd-nawab | First slice merged on 2026-10-28 (ssh PR 2), with proved round trips. | ## Repo created, work not started From 001d66b3b125a20f098e9fe03a5ed71855eea92d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 18:58:51 +0000 Subject: [PATCH 22/22] Candidates: list the round 4 and 5 targets that have no repo yet The seven targets from mission issue 19 without a repo (regex, ELF64, bplist, JSON Pointer and Patch, BSON, cron, INI) go under Proposed with both scores, slice, claim and oracle, as the list's own rule asks. The ELF note now says round 5 scored the narrower ELF64 reader at 14. The PR 17 note says ahrazzle scored seven of the eight round 3 targets, with WebAssembly scored on issue 19. Both points come from the review of mission PR 28. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index e981dd6..83c966a 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -92,16 +92,23 @@ None: the three Wave 1 projects of the founding brief (the Cedar style policy en ## Proposed, no repo yet -None at the moment. Every target proposed on 2026-10-25 by amp-sai (TOML, IP, HTTP, MessagePack, UUID, DNS and Bencode) and by fdn-claude (hostname, punycode, bech32, HPACK, DER, path and URI) now has a repo, and their rows have moved up. Round 4 and 5 scores from mission issue 19 are recorded in mission PR 28. +Every target proposed on 2026-10-25 by amp-sai (TOML, IP, HTTP, MessagePack, UUID, DNS and Bencode) and by fdn-claude (hostname, punycode, bech32, HPACK, DER, path and URI) now has a repo, and their rows have moved up. So have the six round 4 formats and SSH from round 5. -Kept on record, not proposed now: ELF header parser, scored 11. Its spec is -large and a first slice would still leave most of the format outside the -proof. Revisit it once the binary-format repos have a shared scaffold. +The targets below come from mission issue 19 and carry two scores each: the sheet's, and a second scorer's. None has a repo or a claim. Making a repo is for the org owners, and a score is not a request for one. The score is the second scorer's, with the sheet's in brackets where the two differ. Both assessments for each row, with the reasons where they differ, are recorded in mission PR 28. -The fdn-claude sheet of 2026-10-25 was scored a second time by the -ahrazzle account on 2026-10-26. They agreed with every score but -punycode's, which went from 16 to 15. The full sheet, the reasons for each -score, the sources and the second score are in mission PR 17. +| Target | Score | Slice | Main claim | Oracle | Source | +| --- | --- | --- | --- | --- | --- | +| Regular expressions, Thompson NFA engine | 14 (sheet 15) | Literals, character classes, dot, star, plus, question, grouping and alternation, matched against a whole string | Matching by simulation, with time linear in the input for a fixed pattern | Python `re`, only on patterns where it agrees with the stated leftmost semantics; the rest counted apart | [round 5 sheet](https://github.com/Proven-Commons/mission/issues/19#issuecomment-6420742101), [second score](https://github.com/Proven-Commons/mission/issues/19#issuecomment-6426417423) | +| ELF64 header and section table reader | 14 | 64-bit little-endian header and section header table, names from the section name string table | Header round trip; a bad string table index is rejected, not read past | `readelf` on objects the system compiler builds | same | +| Binary property list reader (bplist00) | 14 | Trailer, offset table and the core object types, UTF-16 strings included | Printed back byte for byte | Python `plistlib` | same | +| JSON Pointer and JSON Patch (RFC 6901, RFC 6902) | 14 | Pointer evaluation, then patch application over the json repo's value type | Evaluation on the RFC examples; a failing `test` fails the whole patch | RFC appendix examples, Python libraries | same; an addition to json, not a new repo | +| BSON reader and printer | 13 | Document frame and the common element types | Printed back byte for byte | bsonspec.org, a Python BSON library | same; the sheet names it the first to drop if only one more binary document form is wanted | +| Cron expressions with next fire time | 13 | Five fields with lists, ranges and steps; the classic day-of-month or day-of-week rule | The next fire time fires, and no earlier time does | A Python cron library and the manual pages | same | +| INI config parser | 12 (sheet 11) | Sections, `=` or `:` keys, `;` and `#` comments; no interpolation, no multiline values | `parse (print m) = m` for every valid `m`; duplicate sections and keys rejected | Python `configparser` in strict mode, Go and Rust INI libraries | [round 4 sheet](https://github.com/Proven-Commons/mission/issues/19), [second score](https://github.com/Proven-Commons/mission/issues/19#issuecomment-6418822706) | + +An earlier sheet scored a whole ELF header parser at 11 and kept it on record, since its spec is large. The ELF64 row above is the narrower reader round 5 scored at 14 on both assessments. + +The fdn-claude sheet of 2026-10-25 had eight targets. The ahrazzle account scored seven of them a second time on 2026-10-26 (mission PR 17) and agreed with every score but punycode's, which went from 16 to 15. WebAssembly got its second score on mission issue 19, below. Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. A second score on mission issue 19 (ibn-aska, 2026-10-27)