Z3

Z3는 Microsoft Research에서 개발한 정리 증명기(theorem prover)입니다. MIT 라이선스에 따라 라이선스가 부여됩니다. Windows 바이너리 배포판에는 C++ 런타임 재배포 가능 패키지가 포함되어 있습니다.

Z3가 익숙하지 않다면 여기에서 시작할 수 있습니다.

안정 버전 및 나이틀리 릴리스용 사전 빌드된 바이너리는 여기에서 사용할 수 있습니다.

Z3는 [CMake][3], [vcpkg][4] 또는 [Bazel][5]을 사용하여 빌드할 수 있습니다. [여러 프로그래밍 언어용 바인딩][6]을 제공합니다.

Z3의 다양한 안정 릴리스에 대한 참고 사항은 릴리스 노트를 참조하세요.

빌드 상태

풀 리퀘스트 및 푸시 워크플로

WASM 빌드	Windows 빌드	CI	OCaml 바인딩

결정성 린터	솔버 결정성

예약된 워크플로

Android 빌드	Pyodide 휠 (PyPI)	나이틀리 빌드	크로스 빌드	F* 마스터 빌드

MSVC 정적	MSVC Clang-CL	Z3 캐시 빌드	메모리 안전성	PR 준비 완료 표시

Clang-Tidy 경고 보고서

수동 및 릴리스 워크플로

문서	릴리스 빌드	WASM 릴리스

특수 워크플로

나이틀리 검증	Copilot 설정	Agentics 유지보수	NFV 형식 감사 디스패치

후속 / 댓글 워크플로

결정성 린터 PR 댓글	솔버 결정성 PR 댓글

에이전틱 워크플로

API 일관성	코드 단순화기	릴리스 노트	워크플로 제안	학술 인용

이슈 백로그	메모리 안전성 보고서	SMTLIB 벤치마크 파인더