eth-acl2
EVM Formalizer
A formalization of Ethereum VM in Common Lisp aiming to prove interesting properties of EVM contracts.
An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.
3 stars
3 watching
3 forks
Language: Common Lisp
last commit: about 4 years agoLinked from 1 awesome list
acl2ethereumevmformal-methodsformalizationproofsverification
Related projects:
| Repository | Description | Stars |
|---|---|---|
 mmalvarez/eth-isabelle | A formalization of Ethereum Virtual Machine in Isabelle/HOL with a focus on compiler verification | 33 |
 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 |
 pirapira/eth-isabelle | A formalization of Ethereum's virtual machine using Isabelle/HOL and Lem language | 238 |
 smlxl/evm.codes | An interactive reference and contract viewer for the Ethereum Virtual Machine (EVM) bytecode | 740 |
 av1ctor/evm-txs.mo | A Motoko library for creating and manipulating EVM transactions | 9 |
 takenobu-hs/ethereum-evm-illustrated | An illustrated documentation of Ethereum's virtual machine and its components. | 268 |
 danielvf/evm-contract-draw | A tool for visualizing and analyzing the byte code of Ethereum smart contracts | 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 |
 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 |
| takenobu-hs/haskell-ethereum-assembly | A Haskell-based DSL for generating Ethereum Virtual Machine (EVM) bytecode | 66 |
| ethereum/evmlab | Utilities for interacting with the Ethereum virtual machine | 367 |
 etcdevteam/sputnikvm | An Ethereum Virtual Machine implementation designed to be efficient and adaptable across different blockchain networks. | 280 |
 status-im/nim-evmc | A binary compatible interface between Ethereum Virtual Machines and clients | 15 |