From the article:

[Salt has] [z]ero-cost contracts. requires and ensures clauses are checked at compile time. Proven checks are elided from the binary. Unproven checks become runtime assertions. [...]

Compile-time type-bound proofs. Contracts implied by the type system are proven automatically. requires(x < 256) on a u8 parameter always holds — the compiler knows u8 ∈ [0, 255] and elides the check.