Comment by nemo1618

In essence this lets you verify any property you want for a given function, as long as it can be expressed as a fuzz test. Specifically, you can express your property with an assert, and then prove that it never fires. This is nice because it keeps everything in one language, rather than having to translate the whole program into Rocq and then express your desired property as a Rocq theorem.