이저벨
고차 논리(HOL)를 지원하는 대화형 정리 증명기 도구이다. 사용자가 수학적 증명을 작성하면 이를 기계적으로 검증하며, seL4와 같은 대규모 시스템의 정형 검증 스크립트를 작성하는 데 널리 쓰인다.