[atiernan]

Brings the TLS work of Phase 3 onto main. Supersedes #1. Draft: not to be merged until CI's full verification is green and Alex approves.

What the branch brings

All four crates are at tier 0, as declared in their manifests.

• clazel-tls (tier 0, 0 axioms): TLS 1.3 record and handshake formats, non-PSK key schedule, ClientHello/retry exchange, server selection, initial authentication, bounded connection dispatcher over provider parameters, and the CCS-in-fragment refusal.
• clazel-crypto (tier 0, 12 axioms): libcrux providers for hashing, key schedule, records and X25519, and verified CertificateVerify signatures (ECDSA P-256, RSA-PSS, Ed25519).
• clazel-p384 (tier 0, 6 axioms, over fiat-crypto): verification-only ECDSA P-384 with Wycheproof, NIST CAVP and differential conformance suites.
• clazel-x509: from_unix_seconds (clazel-x509: from_unix_seconds for path validation (3.5b P1), tier 0 #28) with its spec, contract, executable, lemmas, tests and 7 certified mutations (40 mutations in total, all killed).
• Phase3/tls close and cert ext #29 (close and certificate extensions).
• Shared: libcrux/fiat-crypto TCB text in docs/VERIFICATION.md, clazel-p384 optimised in the dev profile, xtask testdata generators for P-384 Wycheproof and CAVP.

clazel-sys is unchanged, the clazel-p384 axioms hash is e9ee88f1...a4e3 (unchanged), and clazel-crypto/src/axioms.rs is identical to the branch before the merge. No tier was changed or raised.

How the merge conflicts were resolved

• clazel-der, clazel-pkcs1: Cargo.toml and README.md from main (tier 2). Both directories are now identical to origin/main. This branch's one commit touching them (4f77bd5, splitting the pkcs1 equivalence lemma) is already reflected in main's independent.rs, so nothing is lost and the tier-2 evidence is untouched.
• clazel-x509: this branch's src/time/{spec,contract,exec,lemmas}.rs, tests/validity_time.rs and mutations.json, because each is main's file plus pure additions (from_unix_seconds; no line of main's was removed). src/lib.rs is main's (keeps pub mod roots). The result differs from main only in those six files.
• Cargo.lock: this branch's, then cargo update --workspace --offline, which only added clazel-html and html5gum. No package changed version relative to either parent.
• docs/DEPENDENCIES.md: all rows from both sides; where both had a row, this branch's (the same version, class shipped where libcrux reaches it, and a longer "why").
• docs/ERRATA.md: every entry from both sides.
• docs/phases/phase-3.md: main's rows for 3.5a and 3.5c (tier 2), 3.6 and 3.7; this branch's for 3.5d, 3.5e and 3.5f; 3.5b merges both (x509 is on main at tier 0, this branch adds from_unix_seconds).
• xtask/src/testdata.rs: every generator from both sides (hash, html5lib, Wycheproof ECDSA and RSA, x509-limbo, CAVP).
• README.md status table, CLAUDE.md, CI: main's, untouched.

Local checks (worktree at the merge commit)

• cargo xtask check: STATIC CHECKS PASSED (clazel-sys audit, escape hatches, 18 documented axioms, tier declarations, dependency allowlist and generated test data all PASS).
• cargo build --workspace, cargo clippy --workspace --all-targets, cargo fmt --check: clean.
• cargo test -p clazel-x509 -p clazel-tls -p clazel-crypto -p clazel-p384 -p clazel-der -p clazel-pkcs1 -p xtask: exit 0, 271 passed, 0 failed.
• Verus per crate from a clean cache: clazel-x509 268 verified, clazel-tls 726, clazel-crypto 44, clazel-p384 133; 0 errors each.
• cargo xtask mutate clazel-x509: 40 mutations, 40 killed by a theorem, 0 survived.

CI has not run yet. Because shared files change (Cargo.lock, workspace manifest, xtask), it will verify every crate.

🤖 Generated with Claude Code