Not the grandparent you were replying to, but from the note added to the original linked issue (emphasis mine):
> Rust's type system is *intended to prevent memory unsafety. Upholding this promise is something we take very seriously*, .... It is a large priority of the Types Team to *fix all type system unsoundnesses* and to work towards there being a solid foundation to minimize the risk of unknown ones.
So, yes, if you have a group who "takes very seriously" the job to "fix all type system unsoundness", I would expect them to utilize some manner of formal proof verification that their type system is mathematically correct up to some defined limit.
> Rust's type system is *intended to prevent memory unsafety. Upholding this promise is something we take very seriously*, .... It is a large priority of the Types Team to *fix all type system unsoundnesses* and to work towards there being a solid foundation to minimize the risk of unknown ones.
So, yes, if you have a group who "takes very seriously" the job to "fix all type system unsoundness", I would expect them to utilize some manner of formal proof verification that their type system is mathematically correct up to some defined limit.