The type-system and forced spec/implementation split both work well to catch errors; you can go further with SPARK [proving] and using Pre- and Post-conditions, type-invariants.