Claim #13 — Verification of rand_pcg::Lcg128CmDxsm64::new (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

Coverage is the twenty-five named bodies on x86_64 under default or serde. Internal word states include zero/even values that usual seed constructors may not produce, but all are valid Rust scalar data; no seed-reachability claim is made. Stream getter behavior for arbitrary increments is proved, but no save/restore identity is claimed for an arbitrary even increment. Aeneas byte-seed/from_seed/seed_from_u64 contracts, Lcg64Xsh32::try_next_u64, buffer filling, RNG callbacks/forking, manual Debug, serde and inherited/external blanket APIs remain outside these Aeneas claims. No period, jump-back interpretation for wrapped negative strides, statistical quality or cryptographic security is established. Other targets and dependency feature combinations were not checked. The Debug supplement is limited to the listed constructor-input families, default formatting and the fixed writer behavior; it does not establish arbitrary internal-state provenance, other Formatter flags, partial-prefix failures, arbitrary writers or all constructor histories. It adds no Aeneas API claim. The Lcg64Xsh32 serde check covers only the fixed sequence protocol, lengths0..2, five Deserialize error stages and successful six-stage serialization. Serialize error stages and arbitrary backend/map/format implementations remain unproved; other PCG serde behavior is covered only by the additional concrete protocols explicitly described here. Arbitrary wire increments are accepted by this check; odd increment or generator invariants are not established. This Kani supplement adds no Aeneas machine claims. The Lcg128Xsl64 result is limited to that32-byte sequence protocol and successful six-callback serialization. Serialize errors, arbitrary backends/map formats, odd increment and nonzero invariants are not established. An earlier unwind20 run failed its unwinding assertion; it is retained as an insufficient-bound attempt, not a successful proof or a crate behavior counterexample. Only the unwind bound changed for the successful run. MCG serde is limited to the fixed sequence protocol, length0..1, three Deserialize callback error stages and successful four-callback serialization; Serialize errors and arbitrary backends/map/formats remain unproved. No odd/nonzero/period invariant follows for its arbitrary wire states. The default-only composition and eight external Rng relations cover constructor-image states, excluding even-increment serde states, zero MCG and all arbitrary private-state histories. They establish relational equivalence to actual TryRng behavior, not independent numeric output, distribution, security or general blanket correctness. A separate seed relation attempt failed in CBMC SMT SSA conversion with map::at before a property verdict; it remains unverified and is not a counterexample. All new evidence is supplemental; the machine count stays25.