정리 증명
주어진 공리와 논리 규칙을 바탕으로 수학적 명제의 참을 입증하는 과정이다. 소프트웨어 검증에서는 코드의 구현이 설계 명세를 정확히 따르는지 논리적으로 확인하는 핵심 단계로 사용된다.