A simple demonstration of formal (mathematical) verification directly motivated by experience with a real-world system.
