Claim #26 — Verification of <rand_xoshiro::Seed512 as Default>::default (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

The Rust compiler, official Charon/Aeneas translation, official Aeneas array/scalar models and Lean kernel are trusted. No source adaptations or local helper axioms are used. Eleven newly covered two/four-word state serializers use a custom executable size_of model with explicit layout evidence only for U32=4 and U64=8 bytes. The original generated Types/Funs remain byte-for-byte official outputs. The Lean evidence class is open; this packet supplies exactly these two primitive instances and guards all eleven generated calls and their frozen elaborated instance bindings. Bool and array types have no supplied evidence and are rejected. This is not a universal type-layout theorem. The three eight-word serializers do not call size_of. Archived independent Kani layout checks confirm the Rust u32/u64 sizes under nightly-2026-08-21; Aeneas extraction uses nightly-2026-09-17. ABI agreement across those compilers and correspondence of Rust layout to the Lean evidence remains an explicit, non-mechanical model bridge. All API and supplementary direct/selector theorems have dependency audits permitting only propext, Classical.choice and Quot.sound. Standard shifts, rotations, wrapping arithmetic and array operations use official Aeneas models, rather than body proofs of Rust std implementations. The nine selector proofs additionally rely on Rust compiler inlining of the exact original API call; retained MIR scopes identify each original TryRng method and Rng wrapper. The selector does not replace or assume an opaque original API: generated native callees are body-proved and no unknown external definitions remain. Seed512 byte-view and iterator initialization proofs use the official array-to-slice and slice-iterator models. The mutable reference model specifies write-back of the fixed-length referent; resizing that referent is not a legal returned-slice operation in safe Rust. The Seed512 constructor supplement separately trusts pinned Kani0.68/CBMC/Z3, its August Rust/compiler memory semantics, exact rand_core0.10.1 and default x86_64 configuration. Enabled unwind70 covers all64-byte comparison/copy loops, without disabled checks, observer, private injection, model or original-source adaptation.