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

Verifereum

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

Відвідати вебсайт (відкривається в новій вкладці)Verifereum на X (відкривається в новій вкладці)Verifereum на GitHub (відкривається в новій вкладці)

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

Certora AutoProver

Про Verifereum

Verifereum підключає смарт-контракти Етеріуму до доведення теорем на базі HOL4, щоб ви могли прагнути до дуже сильних заяв про правильність, коли автоматизованих підходів SMT недостатньо.

Теги

  • Безпека
  • Освіта
  • Формальна верифікація

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

Інформація

Тип
Формальна верифікація
Зірки на GitHub
54
Ліцензія
GPL-3.0
Запис перевірено
червень 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.