Bezpečnost a testování

Certora Prover

Formální verifikace

Zobrazit na GitHubu

Zobrazit další

Kontrol - formal verification tool based on Foundry and KEVM

O 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.

Štítky

Formální verifikace
Verifikace
Bezpečnost

RepozitářCertora

CertoraProver339 (otevře se v nové záložce)

Informace

Typ: Formální verifikace
Hvězdičky na GitHubu: 339
Licence: GPL-3.0
Záznam zkontrolován: září 2026

Podobné nástroje

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.

hax

hax je nástroj pro vysoce spolehlivé překlady velké podmnožiny jazyka Rust do formálních jazyků, jako jsou F* nebo Rocq.

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.