Přejít na hlavní obsah
Bezpečnost a testování

K Semantics of the Ethereum Virtual Machine (EVM)

Formální verifikace

Zobrazit na GitHubu (otevře se v nové záložce)K Semantics of the Ethereum Virtual Machine (EVM) na X (otevře se v nové záložce)

Zobrazit další

hax

O K Semantics of the Ethereum Virtual Machine (EVM)

KEVM je spustitelná sémantika EVM v K-frameworku: namiřte ji na bajtkód, když potřebujete provádění s kontrolou shody, symbolické zkoumání, uvažování o gasu nebo důkazy, které přesně sledují pravidla Etherea.

Štítky

  • Bezpečnost
  • Vzdělávání
  • Analytika
  • Formální verifikace
  • Symbolická exekuce
  • Nástroje pro ladění
  • Verifikace za běhu
  • Vyper

Repozitářruntimeverification

Informace

Typ
Formální verifikace
Hvězdičky na GitHubu
595
Licence
BSD-3-Clause
Záznam zkontrolován
červen 2026

Podobné nástroje

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 povyšuje testy vlastností ve Foundry na důkazy podložené KEVM, takže můžete usilovat o formální záruky s menším množstvím ručně psaných specifikací než u samotného čistého KEVM.

Act

Act

Act je deklarativní specifikační jazyk a sada nástrojů Etherea pro popis veškerého chování EVM programu, aby SMT řešiče, dokazovače teorémů nebo nástroje pro ekonomickou analýzu mohly uvažovat o správnosti na úrovni bajtkódu a kompatibilitě pobídek, včetně automatických důkazů zjemnění vůči konkrétním implementacím.