Güvenlik ve test

Kontrol - formal verification tool based on Foundry and KEVM

Biçimsel doğrulama

Foundry · Eğitim · Yönetişim · Biçimsel doğrulama · Solidity · Çalışma zamanı doğrulaması · Sözleşme dağıtımı · Statik analiz

Sosyal runtimeverification/kontrol(118 ☆)runtimeverification/optimism-ci(4 ☆)runtimeverification/_audits_lidofinance_dual-governance_fork(1 ☆)runtimeverification/yearn-v3-term-vault(0 ☆)runtimeverification/Depeg-swap(0 ☆)runtimeverification/_audits_Ethereum-optimism_pausability(0 ☆)

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.

İlgili kaynaklar

K Semantics of the Ethereum Virtual Machine (EVM)

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.

hax

hax, Rust'ın büyük bir alt kümesinin F* veya Rocq gibi biçimsel dillere yüksek güvenceli çevirileri için bir araçtır.

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.

Verifereum

Verifereum, Ethereum akıllı sözleşmelerini HOL4 destekli teorem ispatına bağlar, böylece otomatik SMT yaklaşımları yeterli olmadığında çok güçlü doğruluk iddialarını hedefleyebilirsiniz.