The /// # Safety documentation section is for publicly unsafe things, to document what the caller's obligations are. It's not about trying to prove to callers that your implementation is sound.
But within the module it does seem reasonable for the safe functions to get comments like "doesn't touch the len or cap fields that unsafe code relies on". That probably depends on the module though, and I don't see much point in a dedicated syntax for comments that lints or rustdoc won't be looking at. Nor can I think of a more precise way of "making them mandatory".
Though at this point it just sounds like we're going back and forth on the same point. An unsafe { } block of code cannot be proven correct without looking at the rest of the module. That's been widely known and understood since well before Rust 1.0 and even proven formally sound. AFAIK the only real questions that have been raised, including proposals like unsafe fields, are essentially different syntaxes atop the same fundamental semantics and mechanisms. It's pretty clear that any workable system of safe vs unsafe code is going to have to rely on some sort of encapsulation boundary.
I feel like your remaining concerns are not so much about technical correctness but more the social aspects of whether this encourages writing unsafe code well. Social engineering ideas have also been discussed in the past so I'll just link to the most relevant posts I have in past threads: