Comment by reddit_clone

This is very interesting.

I am new to Rust and also new to formal verification.

Can someone ELI5 this for me?

(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)