Bezpečnost a testování

Certora Prover

Formální verifikace

Formální verifikace · Verifikace · Bezpečnost

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.

Související zdroje

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.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol povyšuje testy vlastností ve Foundry na důkazy podložené KEVM, takže můžete usilovat o formální záruky s menším množstvím ručně psaných specifikací než u samotného čistého KEVM.

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.

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.

Verifereum

Verifereum propojuje chytré kontrakty Etherea s dokazováním teorémů podporovaným HOL4, takže můžete cílit na velmi silná tvrzení o správnosti, když automatizované přístupy SMT nestačí.