Z3 솔버
Microsoft Research에서 개발한 고성능 제약 충족 문제(SMT) 솔버로, 복잡한 논리식의 충족 가능성을 빠르게 계산하여 소프트웨어 검증 및 AI 추론에 사용된다.