This is cool! Thanks for sharing. I've been wanting something like this for a while

1. I'm curious how this handles I/O? Proving stuff is often really useful for distributed systems where we would like to prove our system behaves correctly under any ordering of I/O operations.

2. How does this compare to just using Rust and some proof tool like Kani or Verus?