Lompat ke konten utama
Keamanan & pengujian

Kontrol - formal verification tool based on Foundry and KEVM

Verifikasi formal

View on GitHub (buka di tab baru)Kontrol - formal verification tool based on Foundry and KEVM on X (buka di tab baru)

See next

Act

About Kontrol - formal verification tool based on Foundry and KEVM

Kontrol mengangkat pengujian properti Foundry ke dalam bukti yang didukung KEVM sehingga Anda dapat mengejar jaminan formal dengan lebih sedikit pekerjaan spesifikasi yang ditulis tangan daripada KEVM mentah saja.

Tag

  • Foundry
  • Edukasi
  • Tata kelola
  • Verifikasi formal
  • Solidity
  • Verifikasi runtime
  • Penyebaran kontrak
  • Analisis statis

Repositoriruntimeverification

Info

Tipe
Verifikasi formal
GitHub stars
126

Sumber daya terkait

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM adalah semantik yang dapat dieksekusi K-framework dari EVM: arahkan ke kode bita saat Anda memerlukan eksekusi yang diperiksa kesesuaiannya, eksplorasi simbolik, penalaran gas, atau bukti yang melacak aturan Ethereum dengan cermat.

hax

hax

hax adalah alat untuk terjemahan jaminan tinggi dari sebagian besar Rust ke dalam bahasa formal seperti F* atau 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.