Sorting algorithms - postcondition is that collection is sorted
Data structures - checking that various internal/external variants hold
Vectors - length <= capacity, accessing nth element has precondition that n is in-bounds, accessing front has precondition that length > 0, etc.
Red-black trees - checking that red-black properties hold (i.e. a red node does not have a red child), checking balance (per Wikipedia, "the path from the root to the farthest leaf is no more than twice as long as the path from the root to the nearest leaf"
Priority queue (implemented by heap), invariant is heap property
Demonstrate Faust's contract-oriented features with some example programs.