Lompat ke konten utama
Keamanan & pengujian

K Semantics of the Ethereum Virtual Machine (EVM)

Verifikasi formal

Lihat di GitHub (buka di tab baru)K Semantics of the Ethereum Virtual Machine (EVM) di X (buka di tab baru)

Lihat selanjutnya

hax

Tentang 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.

Tag

  • Keamanan
  • Edukasi
  • Analitik
  • Verifikasi formal
  • Eksekusi simbolis
  • Alat debugging
  • Verifikasi runtime
  • Vyper

Repositoriruntimeverification

Info

Tipe
Verifikasi formal
Bintang GitHub
595
Lisensi
BSD-3-Clause
Pencantuman ditinjau
Juni 2026

Alat serupa

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.

Kontrol - formal verification tool based on Foundry and KEVM

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.

Act

Act

Act adalah bahasa spesifikasi deklaratif dan rantai alat Ethereum untuk mendeskripsikan semua perilaku program EVM sehingga pemecah SMT, pembukti teorema, atau alat analisis ekonomi dapat menalar tentang kebenaran tingkat kode bita dan kompatibilitas insentif, termasuk bukti penyempurnaan otomatis terhadap implementasi konkret.