All pull requests

Pull requests

• Prove exact trailing sizes, padding and capacity

  #3752·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove primitive layout constructors with recursive mathematical models

  #3751·joshlf opened Oct 2, 2026Member·

  ·
  2

• Compare nested DST sizes with a recursive Rust oracle

  #3749·joshlf opened Oct 2, 2026Member·

  ·
  2

• Model alignment and phase encoding as a bounded mathematical pair

  #3747·joshlf opened Oct 2, 2026Member·

  ·
  2

• Strengthen arithmetic specifications and prove arithmetic corollaries

  #3746·joshlf opened Oct 2, 2026Member·

  ·
  4

• Reuse Aeneas specifications for views and indexed loops

  #3745·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove record construction against independent Rust references

  #3744·joshlf opened Oct 2, 2026Member·

  ·
  2

• Refine recursive record semantics into normalized layouts

  #3743·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove trailing-layout normalization and capacity arithmetic

  #3742·joshlf opened Oct 2, 2026Member·

  ·
  2

• Check native total and partial Aeneas specifications

  #3739·joshlf opened Oct 2, 2026Member·

  ·
  2

• Verify doc-owned specifications over recursive mathematical models

  #3738·joshlf opened Oct 1, 2026Member·

  ·
  3

• Bump Kani to 0.68.0, add pre-roll Kani test, and tighten Kani proof bound

  codex
  #3729·joshlf opened Sep 28, 2026Member·

  ·
  10

• Lint derive-generated code in CI

  #3724·joshlf opened Sep 25, 2026Member·

  ·
  9

• Suppress Clippy lints in derive-generated code

  #3723·joshlf opened Sep 25, 2026Member·

  ·
  9

• [anneal] Refine design contract semantics

  #3719·joshlf opened Sep 24, 2026Member·

  ·
  23

• [pointer] Make TransmuteFrom cast-relative

  #3705·joshlf opened Sep 18, 2026Member·

  ·
  1

  2

• [pointer] Make transmute validity cast-relative

  #3704·joshlf opened Sep 18, 2026Member·

  ·
  1

  1

• [anneal] Define Rust-level verification evidence

  #3702·joshlf opened Sep 18, 2026Member·

  ·
  2

• [anneal] Define verification result semantics

  #3701·joshlf opened Sep 17, 2026Member·

  ·
  2

• [pointer] Use metadata-aware representation proof in transmute helper

  #3699·joshlf opened Sep 17, 2026Member·

  ·
  1

  13

• [pointer] Require same-size proof in transmute helper

  #3694·joshlf opened Sep 17, 2026Member·

  ·
  1

  2

• Allow #[derive(IntoBytes)] to ignore unused const generic parameters

  #3685·barunaniket opened Sep 15, 2026·8 tasks done·

  ·
  1

  13

• Add public constructors for SizeError and ValidityError

  #3678·barunaniket opened Sep 12, 2026·6 tasks done·

  ·
  1

  3

• Clarify pointer contracts and expose iterator capabilities

  #3677·joshlf opened Sep 12, 2026Member·

  ·
  47

• Fix exported macro hygiene and normalize raw field names

  #3676·joshlf opened Sep 12, 2026Member·

  ·
  29