[oconnor663]

This is a formal verification project that has already found some bugs: http://plv.mpi-sws.org/rustbelt/ Interestingly, it's also found some cases where type bounds were unnecessarily restrictive.