증명 실패를 이해하기
자동 증명 도구가 조건을 풀지 못했을 때 원인을 사람이 이해하기 어려울 수 있다. Ivy는 관련 상황을 시각적으로 보여 주고 불변식을 점진적으로 구성하는 흐름을 제공한다. 설명된 상황을 바탕으로 모델의 오류와 불충분한 논증을 구분한다. 시각화가 있다는 사실만으로 증명이 자동 완성되는 것은 아니다.
모듈별 검증과 가정
문제를 작은 구성 요소로 나누고 결정 가능한 논리의 조건으로 표현하는 데 초점을 둔다. 추상 명세와 구현을 refinement로 연결할 수 있다. 한 모듈이 다른 구성 요소에 어떤 계약을 요구하는지 드러내야 전체 결과를 해석할 수 있다. 가정이 실제 환경에서 만족되는지도 검토한다.
명세를 검사에 활용하기
조합 가능한 명세에서 검사 장치와 기대 결과 판정기를 생성해 구현을 시험하는 흐름도 제공한다. 형식 모델의 증명과 실제 구현을 실행한 검사는 서로 다른 역할을 한다. 검사 생성에 사용한 명세와 구현 및 환경의 대응을 유지한다. 도구는 연구용이므로 지원하는 언어 기능과 사용할 배포의 상태를 확인해 적용 범위를 정한다.