Axiom의 검증 커널 내부: BMC, UAP, Lean Replay, 그리고 Proof Vault
Inside Axiom’s Verification Kernel: BMC, UAP, Lean Replay, and the Proof Vault
TL;DR AI
1분핵심 요약
Axiom은 bounded model checking, 자동 복구, Lean 4 재생을 결합해 검증 주장을 재현 가능하게 만든다.
고정된 step limit 안에서 반례를 찾고, UAP 파이프라인이 모델 추출·수정·재증명을 오케스트레이션한다.
Z3는 결정적 SMT 풀이에 쓰이지만, 최종 안전 판정은 Lean 4 proof kernel을 통과해야만 이뤄진다.
이 설계는 단일 SAT/UNSAT 결과보다 재현성과 감사 가능한 증명을 우선해, 잘못된 확신의 위험을 줄인다.
같은 주제
