Harmonic이 C와 Verilog용 형식 검증 도구 Aristotle을 출시했다

Harmonic이 C와 Verilog 코드를 수학적으로 검증하는 Aristotle을 출시했습니다. 개발팀은 코드에서 검증할 속성을 제안받고, 증명 여부와 각 증명의 전제 조건을 확인합니다. 커밋마다 지속적 통합(continuous integration, CI)에서 검증을 실행할 수도 있습니다. 저는 증명 결과와 함께 전제 조건도 보게 한다는 점이 특히 눈에 들어왔습니다. 통과라는 한마디만으로는 무엇을 확인했는지 알기 어렵기 때문입니다.

Vermilion은 Verus의 검증 조건을 Lean 증명으로 바꾸면서 지원 범위와 변환의 형식적 보증에 한계가 있었습니다. Aristotle도 증명 결과와 함께 전제 조건을 확인하게 합니다. 두 도구는 코드 검증을 자동화하는 만큼, 도구가 실제로 보증하는 경계를 개발자가 읽어야 한다는 점에서 맞닿습니다.

코드 리뷰와 테스트는 가능한 동작의 일부를 살핍니다. Aristotle은 지정한 시스템 안의 모든 가능한 입력에서 속성이 성립하는지 증명합니다. 검증할 속성을 제안받고 커밋마다 CI로 이어지는 점도 반갑습니다.

다만 증명 범위는 지정한 시스템 안으로 정해집니다. 또 증명마다 전제 조건이 있으므로, 그 조건이 실제 요구사항과 다르면 증명 성공이 원하는 보증을 뜻하지 않을 수 있습니다.

작은 코드 범위에서 검증 속성 하나를 골라, Aristotle의 증명 결과와 그 전제 조건이 실제 요구사항과 맞는지 대조해 보십시오. 조건이 맞다면 커밋마다 검증하도록 설정하고, 조건을 바꿨을 때 증명 결과가 어떻게 달라지는지도 시험해 보십시오.

코드를 검증할 때 요구사항과 전제 조건 중 무엇을 먼저 대조하십니까?