It would be lovely if Kani and/or Prusti could cope with more realistic code, but they are where my current hopes lie in eliminating the verification gap. The p

It would be lovely if Kani and/or Prusti could cope with more realistic code, but they are where my current hopes lie in eliminating the verification gap. The proof is built from (very!) simple functions written in a subset of Rust. If that manages to get to you all the way to the end result, then there was no gap. https://github.com/model-checking/kani https://github.com/model-checking/kani http://prusti.org/ http://prusti.org/