Перейти до основного вмісту
Безпека та тестування

K Semantics of the Ethereum Virtual Machine (EVM)

Формальна верифікація

Переглянути на GitHub (відкривається в новій вкладці)K Semantics of the Ethereum Virtual Machine (EVM) на X (відкривається в новій вкладці)

Дивитися далі

hax

Про K Semantics of the Ethereum Virtual Machine (EVM)

KEVM — це виконувана семантика EVM у K-framework: вкажіть їй на байт-код, коли вам потрібне виконання з перевіркою відповідності, символьне дослідження, міркування щодо газу або доведення, які тісно відстежують правила Етеріуму.

Теги

  • Безпека
  • Освіта
  • Аналітика
  • Формальна верифікація
  • Символьне виконання
  • Інструменти налагодження
  • Верифікація під час виконання
  • Vyper

Репозиторійruntimeverification

Інформація

Тип
Формальна верифікація
Зірки на GitHub
595
Ліцензія
BSD-3-Clause
Запис перевірено
червень 2026 р.

Схожі інструменти

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 на доведення на базі KEVM, щоб ви могли досягати формальних гарантій з меншим обсягом написаних вручну специфікацій, ніж при використанні лише чистого KEVM.

Act

Act

Act — це декларативна мова специфікацій та набір інструментів Етеріуму для опису всіх способів поведінки програми EVM, щоб SMT-вирішувачі, системи доведення теорем або інструменти економічного аналізу могли аналізувати коректність на рівні байт-коду та сумісність стимулів, включаючи автоматичні доведення уточнень для конкретних реалізацій.