아마존 사이언스, Rust 정형 검증 도구 Verus 소개... HN에서는 "결국 Z3에 증명 던지는 것뿐" 지적

Verus 딱 내가 찾던 거임. 예전에 AllConcur를 Go로 포팅하려 했는데 TLA+랑 C로 되어 있어서, TLA+를 C로 컴파일하지 않고서야 구현을 어떻게 믿어야 하는지 이해가 안 갔음. Verus는 Rust랑 같이 컴파일되고 통합되니 훨씬 낫더라.

TLA+ 옹호자들한테 늘 불만인 게 그거임. 특정 알고리즘에 대한 이론적 증명이랑 실제 프로덕션 구현이 따로 논다는 점. 그래서 나는 FStart나 Dafny처럼 증명에서 코드를 생성하거나, SPARK, Frama-C, Verus처럼 언어에 붙어 있는 도구를 밀음.

신기한데, Rust 코드 안에서 수학 증명을 직접 검증한다는 거임? 이게 어떻게 가능한지 원리를 아는 사람 있나?

증명 문장이랑 프로그램 정보를 SMT 문제로 바꿔서 Z3에 돌리는 방식임. SPARK/Ada나 Dafny도 비슷하게 동작하고 문서는 더 잘 되어 있으니 입문용으로 그쪽부터 보는 것도 좋음. Dafny 책이랑 SPARK 무료 튜토리얼도 있음.

그냥 증명 의무를 Z3 같은 SMT 솔버에 던지는 것뿐임. Verus만의 특별한 건 없고 Dafny, Frama-C가 하는 것과 같은데 대상이 Rust일 뿐임. 글도 대부분 Verus 고유 내용이라기보다 저자 연구랑 AWS 작업 홍보에 가까움.

명세 자체가 틀리면 어쩌려고? 수학 명세의 정확성을 코드보다 빠르게 증명할 방법이 있나? API랑 언어가 계속 바뀌는데. 정형 검증은 절대 안 될 거라고 봄. 올바른 코드도 못 쓰는 사람이 올바른 수학 명세는 쓴다는 주장부터가 이상함.

명세 정확성은 기밀성이나 무결성처럼 잘 받아들여지는 기준을 만족하는지 보이면 됨. 그건 보통 마지막 검증 단계에서 하고, AWS가 EC2 Nitro 하이퍼바이저로 실제로 했음.

그러면 "구현도 명세도 틀렸다"에서 "명세만 틀렸다"로 옮겨가는 건데, 증명할 수 있는 것만이라도 증명하는 게 낫지. 완벽을 good의 적으로 만들 필요는 없음.

Microsoft의 Aeneas도 참고할 만함. Rust를 Lean으로 옮겨서 검증하는 프로젝트임.