Chuyển đến nội dung chính
Bảo mật & kiểm thử

Kontrol - formal verification tool based on Foundry and KEVM

Xác minh hình thức

Xem trên GitHub (mở trong tab mới)Kontrol - formal verification tool based on Foundry and KEVM trên X (mở trong tab mới)

Xem tiếp

Act

Giới thiệu về Kontrol - formal verification tool based on Foundry and KEVM

Kontrol nâng tầm các bài kiểm thử thuộc tính của Foundry thành các bằng chứng được hỗ trợ bởi KEVM để bạn có thể theo đuổi các đảm bảo hình thức với ít công việc viết đặc tả thủ công hơn so với chỉ dùng KEVM thô.

Thẻ

  • Foundry
  • Giáo dục
  • Quản trị
  • Xác minh hình thức
  • Solidity
  • Xác minh thời gian chạy
  • Triển khai hợp đồng
  • Phân tích tĩnh

Các kho lưu trữruntimeverification

Thông tin

Loại
Xác minh hình thức
Số sao trên GitHub
127
Giấy phép
BSD-3-Clause
Đã đánh giá mục niêm yết
tháng 6 năm 2026

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

K Semantics of the Ethereum Virtual Machine (EVM)

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

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

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.