Repository navigation
Conversation
Every SERVER testcase of x509-limbo with a DNS or IP peer name through both engines, signatures accepted on both sides. 23 of 9,791 differ, each listed with its reason. The corpus plumbing moves to tests/limbo/common.rs so both suites share it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The corpus's generated fields are only all used there, and it reports the clazel-conformance summary line xtask reads. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Stacks this branch on #126. Its wildcard change makes webpki and us agree on webpki::san::public-suffix-private-namespace-wildcard-san, so 22 testcases differ, not 23. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A second transcription, from ITU-T X.509 (10/2019), X.690, X.680, X.501, X.520, X.681 and RFC 6125, written without reading the crate's first one. Spec functions only, with examples Verus evaluates; no equivalence proof yet, and the tier stays 0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ns_match theorem_certificate_equivalence on a domain of 13 numbered exclusions, theorem_dns_match_is_rfc_6125 with its own, and theorem_signature_algorithms. equivalence_examples.rs evaluates an input for each disagreement it can and one certificate inside the domain. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The mutant spki-parse-classifies-ec removes the only call to classify_ec_public_key reachable from equivalence_structures. The hide in theorem_spki_back still names it, so Verus panics with ill-typed AIR (undeclared fuel variable) and the mutation run reports that the mutated crate does not build. Without the hide the mutant is an ordinary failed proof. The module still verifies on the real spec; the whole crate and the mutation suite have not been rerun locally. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ns.rs Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…s read Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…he leaf check Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…tion path Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…pdate the docs Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
x509: close the independent transcription's coverage gaps (stacked on #132)
…dence-to-main # Conflicts: # docs/ERRATA.md
atiernan
requested a deployment
to
full-verification
November 14, 2026 01:29 — with 
GitHub Actions
Waiting
GitHub Actions
Waiting
This branch is waiting to be deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Brings the X.509 tier 2 evidence to
main. No tier changes:clazel-x509stays attier = 0.Why this is needed
#110, #130, #132 and #135 were stacked: each one merged into the one below it, and #110 merged into
phase3/wildcard-icannon 2026-11-07. Butphase3/wildcard-icannhad already reachedmainthrough #126 on 2026-11-06. So none of these four PRs is onmain: the rustls-webpki differential, the independent transcription of certificates and host matching, its equivalence proofs, or the coverage-gap proofs. This PR is that branch withorigin/mainmerged in.What changed in the merge
docs/ERRATA.md. Both sides only appended entries at the same place. I kept all of them: the three X.509 entries from this branch first, thenmain's 18. Each entry is unchanged. The X.509 entries' sharedReported upstream: not yet.line is restored, and the count is 19 at the merge base + 18 frommain+ 3 from this branch = 40.Cargo.lock,docs/DEPENDENCIES.md,docs/phases/phase-3.md).mainis the 16 commits of the stack plus the merge: 34 files.Verification
cargo xtask check:STATIC CHECKS PASSEDon the merge commit.cargo xtask verify --changed: running locally in WSL, no result yet.Cargo.lockchanges, so it selects every crate. I'll add the result here. x509: close the independent transcription's coverage gaps (stacked on #132) #135's localcargo xtask mutate clazel-x509never finished (WSL ran out of memory), so the x509 mutation result has to come from CI.main. The proof jobs need afull-verificationreviewer's approval.Still needed for tier 2 (not in this PR)
spkikey classification, from a session that has not read the crate's spec, then its equivalence proof by a different author.NameConstraintssequence: the crate accepts it and the transcription refuses it (x509: close the independent transcription's coverage gaps (stacked on #132) #135).subject_rule, cA flagged critical,policyConstraintson a target,name_types_distinct.🤖 Generated with Claude Code