(1) A formal technique used to prove mathematically that a computer program satisfies its specified requirements.~(2) A proof that results from applying the technique in (1).