[kixelated]

Skeleton for the follow-up to the rind launch post: rind, but formally verified. It covers every correctness mechanism, not just the proofs. Headings are the outline; bullets are notes and PR links to write from. Every TODO is yours to fill.

Facts gathered

Source: moq-dev/rind origin/main 0f4e45f0 (2026-11-12), plus proofs/README.md, TESTING.md and quest/.

• Proof stack:

  • Charon and Aeneas translate the Rust into Lean 4.
  • rind's own assembly is proven in HOL Light on s2n-bignum's models.
  • Proofs from s2n-bignum, Vale/HACL* and aws-lc-verification are imported as axioms.
  • admin/prove bytes ties the proofs to the shipped object code.

• What "verified" means here: functional correctness only. Memory safety and panic-freedom are not proven. Constant time is proven only for the asm compares and s2n-bignum's _SAFE routines.

• The launch post needs a caveat. It says AES-GCM is verified, but it's proven only on x86_64 AES-NI. VAES CPUs and aarch64 are not covered.

• Five checks per primitive, enforced by admin/testing:

  • test vectors
  • differential fuzzing against aws-lc-rs
  • constant time: ctgrind, BINSEC, a static scan, and dudect/Marvin
  • zeroing
  • memory safety: guard pages, Miri, ASan, an ABI harness

  On top of that: cross-arch runs (SDE plus qemu), mutation testing, and the adversarial REVIEW.md.

• Roadmap: m3 is SHA-NI SHA-256. m4 is the hot tiers, 24 quests. m5 is the cold tiers.

Waiting

• Keeping the post current: proofs land daily, so the scoreboard and roadmap sections will go stale. Refresh them from rind main right before publishing (the skeleton has TODOs). I can also run a recurring refresh of this branch while rind quests land; say if you want that.
• Coverage chart: the skeleton reuses <Coverage /> and the launch post's cover. libraries.json needs regenerating from current rind for this post. Should it stay shared with the launch post or be split?

Public API and wire impact

None.

Validation

bunx biome check and bun astro build --mode staging pass, and /blog/rind-verified renders with the coverage chart.

Models

Size: S
Implementer: Claude Code, claude-opus-5-5, unknown effort

(Written by Opus 5.5)

🤖 Generated with Claude Code