evmverif
EVM verifier
A framework for verifying smart contract code on the Ethereum Virtual Machine
An EVM code verification framework in Coq
44 stars
12 watching
8 forks
Language: Coq
last commit: about 8 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 runtimeverification/avm-semantics | A tool for formally verifying Algorand smart contracts' behavior using property-based testing and symbolic execution | 15 |
 pipermerriam/py-evm | A Python implementation of the Ethereum Virtual Machine. | 40 |
| pirapira/eth-isabelle | A formalization of Ethereum's virtual machine using Isabelle/HOL and Lem language | 237 |
 vorot93/evmodin | An implementation of the Ethereum Virtual Machine in Rust, with support for resumability and gas metering. | 162 |
 ethereum/evmone | An implementation of the Ethereum Virtual Machine | 858 |
 valida-xyz/valida | A virtual machine for efficient and modular verification of program executions using Stark-based verification methods. | 290 |
 fvictorio/evm-puzzles | A collection of puzzles to test Ethereum Virtual Machine (EVM) functionality by solving specific transaction-related challenges. | 816 |
 etcdevteam/sputnikvm | An Ethereum Virtual Machine implementation designed to be efficient and adaptable across different blockchain networks. | 279 |
 vellvm/vellvm | A formal verification project of the LLVM compiler's semantics using Coq proof assistant. | 400 |
| ethereum/evmlab | Utilities for interacting with the Ethereum virtual machine | 366 |
 smlxl/evm.codes | An Ethereum Virtual Machine opcode reference tool with a web-based interface. | 734 |
 rust-ethereum/evm | A flexible, customizable, and portable implementation of the Ethereum Virtual Machine | 1,190 |
 0xpolygonhermez/zkevm-prover | A high-performance prover that generates proofs for Ethereum Virtual Machines (EVM) transactions | 226 |
 au-cobra/concert | A framework for verifying smart contracts in Coq using formal methods and property-based testing. | 114 |
 danielvf/evm-contract-draw | A tool for visualizing and analyzing the byte code of Ethereum smart contracts | 122 |