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

Certora AutoProver

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

Переглянути на GitHub (відкривається в новій вкладці)

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

K Semantics of the Ethereum Virtual Machine (EVM)

Про Certora AutoProver

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Теги

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

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

Інформація

Тип
Формальна верифікація
Зірки на GitHub
17
Ліцензія
GPL-3.0
Запис перевірено
вересень 2026 р.

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

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.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol перетворює тести властивостей Foundry на доведення на базі KEVM, щоб ви могли досягати формальних гарантій з меншим обсягом написаних вручну специфікацій, ніж при використанні лише чистого KEVM.