This process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/. It has not y

This process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/. It has not yet achieved the kind of tight integration with the source language that stuff like Creusot has, but everyone would like it to move in that direction :) For the specific case of Vec (and a few other types--e.g. Cell, Mutex, etc.), as I mentioned, a recent paper by xavxav actually proves that the important parts of the unsafe implementation of Vec do actually fulfill the signatures that are used by the CreuSAT proof. This is part of https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper..., which I believe won the distinguished paper award at this year's PLDI!