Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

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

Sosial runtimeverification/evm-semantics(586 ☆)

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.

Related resources

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.

hax

hax adalah alat untuk terjemahan jaminan tinggi dari sebagian besar Rust ke dalam bahasa formal seperti F* atau Rocq.

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.

Verifereum

Verifereum menghubungkan kontrak pintar Ethereum ke pembuktian teorema yang didukung HOL4 sehingga Anda dapat menargetkan klaim kebenaran yang sangat kuat ketika pendekatan SMT otomatis tidak cukup.