Indeed, Creusot itself is not formally verified, but we have verified the metatheory in our paper RustHornBelt: https://people.mpi-sws.org/~dreyer/papers/rustho

Indeed, Creusot itself is not formally verified, but we have verified the metatheory in our paper RustHornBelt: https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.... Actually verifying the translation that Creusot produces would definitely be interesting future work, but I'm not sure it's where the best 'bang for the buck' is found right now, though I try to ensure the underlying translation would remain simple to formalize.