Repository navigation

Verify the safety of core::slice functions with VeriFast (Challenge 17) - #742

Open

paulocsanz wants to merge 15 commits into

model-checking:mainfrom

paulocsanz:challenge17-verifast-slice

Open

Verify the safety of core::slice functions with VeriFast (Challenge 17)#742
paulocsanz wants to merge 15 commits into
model-checking:mainfrom
paulocsanz:challenge17-verifast-slice

Commits on Oct 27, 2026
- VeriFast proof of core::slice (Challenge 17): contracts for the 10 unsafe fns and safety proofs for the 27 safe abstractions
  
  Paulo Cabral Sanz
  authored and
  paulocsanz
  committed
  796361a
- verifast-proofs/core/slice: build the noslice core sysroot from VeriFast's own toolchain rust-src
  paulocsanz
  committed
  0096870
- verifast-proofs/core/slice: close the open-ended axioms
  paulocsanz
  committed
  1dd4857
- verifast-proofs/core/slice: README: list the sysroot core edits made by verify.sh
  paulocsanz
  committed
  eb18363
- verifast-proofs/core/slice: add a negative test (mod.rs-negative)
  paulocsanz
  committed
  8221187
Commits on Oct 28, 2026