Certora AutoProver

hax는 Rust의 큰 하위 집합을 F* 또는 Rocq와 같은 공식 언어로 높은 보증(high assurance)을 가지고 번역하기 위한 도구입니다.

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

Kontrol은 Foundry 속성 테스트를 KEVM 기반 증명으로 끌어올려, 순수 KEVM만 사용할 때보다 수작업 사양 작성 작업을 줄이면서 정형 검증 보장을 추구할 수 있게 해줍니다.