Counterexamples in Safe Rust

This is a WIP will be updated.