While continuing to work on the next version of the mental model to incorporate the concept of robustness (the composable version of super-safe) which significantly improves the model, I realized that it should not be recommended to document robustness unless a significant amount of unsafe code depends on it. The reason is that it would force unsafe reviewers to review those properties even though they may not directly affect any unsafe code in the actual dependency tree of the project relying on this unsafe review, thus wasting effort according to that project.
Even in a world where everybody uses and trusts a single cargo-vet registry (thus never wasting effort), if no unsafe code in the world relies on this robustness at the moment, then that's still unnecessary work. The robustness documentation should only be added when some unsafe code in the cargo-vet registry depends on it. In a world where there are multiple cargo-vet registries, this should be decided per registry and becomes a bit messier. So I can see how preemptively documenting a function as robust (i.e. moving part of the correctness documentation to a # Robustness section or doing the same in the cargo-vet review system to not burden the crate owner) is a bad idea. I still believe doing it once there is a legitimate use, would bring value (even if it's just in the review system and not in the crate, to transfer burden from crate owners to unsafe reviewers).