I'm very much in favor of machine-checkable safety annotations in some form, and I like the idea of getting there by refining the existing human-readable free-form safety comments.
However, I would like to ask how your scheme would handle a lengthy unsafe code block whose safety presumes the well-formedness of a complex data structure produced on the other side of an FFI boundary. This is the most common reason for unsafe in the code I tend to write, and previous proposals (e.g. the "Unsafe Reasons" pre-RFC) have involved adding so many annotations inside the unsafe block that they would make it difficult to follow the actual logic of the code within.
I posted a concrete example of the kind of code I'm talking about in the "Unsafe Reasons" pre-RFC thread; the full code from which that example was cut down can be found here and here.