Verify safety of Vec IntoIter functions with VeriFast (Challenge 24)#562

Draft

jrey8343 wants to merge 9 commits intomodel-checking:mainfrom

jrey8343:challenge-24-vec-pt2

Commits on Feb 8, 2026

Verify safety of Vec functions (Challenge 23)
jrey8343
committed

Commits on Feb 11, 2026

Apply upstream rustfmt formatting via check_rustc.sh --bless
jrey8343
committed

Commits on Mar 15, 2026

Make Ch23 Vec pt1 harnesses unbounded

jrey8343
and
claude
committed

Commits on Mar 16, 2026

Add VeriFast proof infrastructure with custom &[T] slice support

jrey8343
and
claude
committed