eth-isabelle
EVM formalizer
A formalization of Ethereum Virtual Machine in Isabelle/HOL with a focus on compiler verification
A Lem formalization of EVM and some Isabelle/HOL proofs
33 stars
5 watching
6 forks
Language: Isabelle
last commit: about 5 years ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
 pirapira/eth-isabelle | A formalization of Ethereum's virtual machine using Isabelle/HOL and Lem language | 238 |
 zchn/eth-acl2 | A formalization of Ethereum VM in Common Lisp aiming to prove interesting properties of EVM contracts. | 3 |
 0xpolygonhermez/zkevm-prover | A high-performance prover that generates proofs for Ethereum Virtual Machines (EVM) transactions | 229 |
 ethereum/evmone | An implementation of the Ethereum Virtual Machine | 872 |
 leonardoalt/tinyzkevm | A proof-of-concept implementation of a small subset of the Ethereum Virtual Machine (EVM) inside a Smart Contracting Language (SNARK), using ZoKrates. | 46 |
 nervous-systems/sputter | An implementation of the Ethereum Virtual Machine | 122 |
 runtimeverification/evm-semantics | Provides a formal model of the Ethereum Virtual Machine (EVM) semantics in the K programming language. | 509 |
 zama-ai/fhevm | A Solidity library that enables developers to write confidential smart contracts on the EVM using fully homomorphic encryption. | 436 |
| ethereum/evmlab | Utilities for interacting with the Ethereum virtual machine | 367 |
 rust-ethereum/evm | A flexible, customizable, and portable implementation of the Ethereum Virtual Machine | 1,200 |
 smlxl/evm.codes | An interactive reference and contract viewer for the Ethereum Virtual Machine (EVM) bytecode | 740 |
 bluealloy/revm | Rust implementation of an Ethereum Virtual Machine with focus on speed and simplicity. | 1,685 |
 vorot93/evmodin | An implementation of the Ethereum Virtual Machine in Rust, with support for resumability and gas metering. | 161 |
 pipermerriam/py-evm | A Python implementation of the Ethereum Virtual Machine. | 40 |
 av1ctor/evm-txs.mo | A Motoko library for creating and manipulating EVM transactions | 9 |