Перейти к основному контенту
Безопасность и тестирование

Kontrol - formal verification tool based on Foundry and KEVM

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

Посмотреть на GitHub (открывается в новой вкладке)Kontrol - formal verification tool based on Foundry and KEVM на X (открывается в новой вкладке)

Смотреть далее

Act

О Kontrol - formal verification tool based on Foundry and KEVM

Kontrol преобразует тесты свойств Foundry в доказательства на базе KEVM, чтобы вы могли получать формальные гарантии с меньшим объемом ручного написания спецификаций, чем при использовании только чистого KEVM.

Теги

  • Foundry
  • Обучение
  • Управление
  • Формальная верификация
  • Solidity
  • Верификация во время выполнения
  • Развертывание контрактов
  • Статический анализ

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

Информация

Тип
Формальная верификация
Звезды на GitHub
127
Лицензия
BSD-3-Clause
Информация проверена
июнь 2026 г.

Похожие инструменты

K Semantics of the Ethereum Virtual Machine (EVM)

K Semantics of the Ethereum Virtual Machine (EVM)

KEVM — это исполняемая семантика EVM на базе K-framework: используйте ее с байт-кодом, когда вам нужно выполнение с проверкой соответствия, символьное исследование, анализ газа или доказательства, которые строго следуют правилам Эфириума.

hax

hax

hax — это инструмент для высоконадежной трансляции большого подмножества Rust в формальные языки, такие как F* или Rocq.

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.