Contracts
Defects relating to contracts — the preconditions, postconditions, and assertions that state what a piece of code requires and guarantees. A contract that is violated means the code ran outside the bounds it promised to honour; a contract for which no proof is available means the guarantee is merely asserted, neither established nor checked, and the verification it was meant to enable cannot proceed.