KEVM

Open Source

Formal semantics of the EVM in the K Framework. Enables rigorous verification of smart contract bytecode against formal specifications.

About

KEVM is a complete formal semantics of the Ethereum Virtual Machine defined in the K Framework. It enables formal verification of smart contract bytecode by providing a mathematically precise definition of EVM execution. KEVM is used by Runtime Verification for auditing and can verify properties directly against compiled bytecode, catching bugs that source-level analysis might miss.