An unsafe function in Rust is a function that requires its caller to uphold invariants the compiler cannot check. The signature does not say what those invariants are. The body does not check them. They live in a comment, or in the documentation, or in the head of whoever wrote the function.
This is fine until you want to verify that the function is actually safe under its stated assumptions. To do that, you have to make the assumptions machine-readable. This is what a precondition is.
the shape of a precondition
A precondition is a boolean expression in terms of the function's arguments and the program state that must hold at the call site. For unchecked_add on signed integers, the precondition is "the addition does not overflow":
#[requires(!self.overflowing_add(rhs).1)]
pub const unsafe fn unchecked_add(self, rhs: Self) -> SelfThe #[requires] attribute is read by a verifier. At a verification call site, the precondition is asserted to hold over all symbolic inputs the verifier generates. If any input violates it, the verifier reports a counterexample. If no input violates it, the function's safety is proved with respect to that precondition.
where preconditions come from
Three sources, in order of preference.
Existing checks in the function body. Many unsafe functions already contain a debug-time check that mirrors the precondition — an assert_unsafe_precondition! or a manual debug_assert. The precondition is whatever that check is testing. Lifting it into a #[requires] attribute is mechanical and lossless.
The SAFETY comment. Rust convention is to document the safety contract of an unsafe function in a // SAFETY: comment above the call. These comments are written for humans, but they almost always translate cleanly into a boolean expression. "The pointer must be non-null and aligned" becomes !ptr.is_null() && ptr.is_aligned().
The language reference and intrinsic documentation. When neither of the above exists, the precondition has to be reconstructed from the reference and the spec for the underlying intrinsic. This is the slowest path and the most error-prone — small omissions become silent verification gaps. It also tends to be where the subtlest mismatches between documentation and actual behavior hide.
where preconditions go wrong
The most common failure is a precondition that is weaker than the actual safety contract. The verifier reports success because the assertion holds under the stated assumption, but the function is still unsound because the assumption itself is incomplete. The verifier did its job. The contract was wrong.
The second most common failure is a precondition that is stronger than necessary. The verifier reports success, but real callers cannot satisfy the contract, so the function becomes unverifiable in practice. This is less dangerous but still a defect — verification is supposed to certify the function as it is, not as a more conservative version of itself.
The third failure mode is subtler: the precondition references types or values that the verifier cannot reason about precisely. For example, casting i32::MAX to f32 produces 2147483648.0, not 2147483647.0, because f32 lacks the mantissa bits to represent the exact value. A precondition that says "the float is at most i32::MAX as f32" therefore admits a value that is outside the integer's range. The contract is internally consistent and externally wrong.
A related issue: preconditions lifted directly from debug assertions are not always complete. The debug assertion may check the most common failure case without covering every condition that leads to undefined behavior.
the discipline
Writing preconditions is mostly the discipline of refusing to assume what you have not stated. Every assumption you carry in your head about how the function will be called is a potential gap in the contract. The verifier will not catch the gap, because the gap is in the contract itself. The only way to find it is to read the precondition out loud and ask, for each clause, "is there an input that satisfies this and still breaks the function?" If yes, the precondition is incomplete. If no, it is at least sound.
This is slow work, but without it, verification never really gets past "the function is safe if the thing we forgot to state happens to be true."