Z3 정리 증명기
Microsoft Research에서 개발한 고성능 SMT(Satisfiability Modulo Theories) 솔버로, 복잡한 논리식의 만족 여부를 판별한다. 소프트웨어 분석 및 검증 문제에서 제약 조건을 수학적으로 확인하고 반례를 찾는 데 사용된다.