Bảo mật & kiểm thử

Certora Prover

Xác minh hình thức

Xem trên GitHub

Xem tiếp

Kontrol - formal verification tool based on Foundry and KEVM

Giới thiệu về Certora Prover

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.

Thẻ

Xác minh hình thức
Xác minh
Bảo mật

Kho lưu trữCertora

CertoraProver339 (mở trong tab mới)

Thông tin

Loại: Xác minh hình thức
Số sao trên GitHub: 339
Giấy phép: GPL-3.0
Đã đánh giá mục niêm yết: tháng 9 năm 2026

Các công cụ tương tự

K Semantics of the Ethereum Virtual Machine (EVM)

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

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.

Act

Act là ngôn ngữ đặc tả khai báo và chuỗi công cụ của Ethereum để mô tả tất cả các hành vi của một chương trình EVM để các bộ giải SMT, trình chứng minh định lý hoặc các công cụ phân tích kinh tế có thể lập luận về tính đúng đắn ở cấp độ mã byte và khả năng tương thích khuyến khích, bao gồm các bằng chứng tinh chỉnh tự động đối với các triển khai cụ thể.