In computer science, the act of formally proving an algorithm's correctness (i.e. that all possible input yields results that conform to the specification). A very boring and tiresome task.