Ana içeriğe atla
Güvenlik ve test

K Semantics of the Ethereum Virtual Machine (EVM)

Biçimsel doğrulama

GitHub'da görüntüle (yeni sekmede açılır)X üzerinde K Semantics of the Ethereum Virtual Machine (EVM) (yeni sekmede açılır)

Sonrakini gör

hax

K Semantics of the Ethereum Virtual Machine (EVM) Hakkında

KEVM, EVM'nin K-framework yürütülebilir semantiğidir: uygunluk kontrollü yürütme, sembolik keşif, gaz muhakemesi veya Ethereum'un kurallarını yakından izleyen kanıtlara ihtiyacınız olduğunda onu baytkoda yönlendirin.

Etiketler

  • Güvenlik
  • Eğitim
  • Analitik
  • Biçimsel doğrulama
  • Sembolik yürütme
  • Hata ayıklama araçları
  • Çalışma zamanı doğrulaması
  • Vyper

Deporuntimeverification

Bilgi

Tür
Biçimsel doğrulama
GitHub yıldızları
595
Lisans
BSD-3-Clause
Listeleme incelendi
Haziran 2026

Benzer araçlar

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, Foundry özellik testlerini KEVM destekli kanıtlara yükseltir, böylece yalnızca ham KEVM'den daha az elle yazılmış spesifikasyon çalışmasıyla biçimsel garantilerin peşine düşebilirsiniz.

Act

Act

Act, SMT çözücülerin, teorem kanıtlayıcıların veya ekonomik analiz araçlarının somut uygulamalara karşı otomatik iyileştirme kanıtları da dahil olmak üzere baytkod düzeyinde doğruluk ve teşvik uyumluluğu hakkında akıl yürütebilmesi için bir EVM programının tüm davranışlarını tanımlamaya yönelik Ethereum'un bildirimsel spesifikasyon dili ve araç zinciridir.