State of affairs of verification of rust programs

Stream: Program verification

[April Gonçalves]

I’m interested in verifying some crucial piece of rust program that takes into account ownership, lifetimes, etc. The code implements theories that have been formally proved, however, the translation from math to rust feels flimsy (even with a test suite, but no quickcheck yet). I found Sebastian Ullrich’s master thesis, but it uses lean 3 and it’s from 2016.

[April Gonçalves]

!

[Sebastian Ullrich]

Yes, see https://github.com/AeneasVerif/aeneas for a Lean 4-compatible approach!