hol-light

고차 논리(Higher-Order Logic)를 기반으로 하는 상호작용형 정리 증명기이다. 매우 작은 신뢰 커널을 가지고 있어 증명 과정의 오류 가능성을 최소화하며, 복잡한 암호화 알고리즘의 어셈블리 수준 검증에 사용된다.