Verifereum

KEVM là ngữ nghĩa thực thi K-framework của EVM: hãy trỏ nó vào mã byte khi bạn cần thực thi được kiểm tra sự tuân thủ, khám phá tượng trưng, lập luận về gas hoặc các bằng chứng theo dõi chặt chẽ các quy tắc của Ethereum.

hax là một công cụ để dịch với độ đảm bảo cao một tập hợp con lớn của Rust sang các ngôn ngữ hình thức như F* hoặc Rocq.

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.