ACL2 Ethereum Project



The goal of the ACL2 Ethereum project is to formally specify and synthesize/implement a full Ethereum client using the ACL2 theorem prover and the APT toolkit.

The first phase of the project, starting in October 2018, is to create a high-assurance command-line wallet suitable for cold storage of keys and transaction signing. This requires specifications and implementations of cryptographic algorithms such as Keccak-256, SHA-256, HMAC-SHA512, and secp256k1, and HD wallet standards such as BIP-32, BIP-39, BIP-43, and BIP-44. In addition, we will be synthesizing code for RLP encoding/decoding and Modified Merkle Patricia Tree processing.

Code created during the project, and supporting libraries that we are in the process of open-sourcing, will be published primarily under the Community Books directory of ACL2.

This project is motivated by the grand vision that all software development should incorporate formal methods and have proofs. More urgently, cryptocurrencies should have a diversity of formal methods brought to bear on them, since the consequences of vulnerabilities are so dire.

On the Suitability of ACL2 and APT

ACL2 is a theorem prover whose language can express both high-level declarative specifications and efficiently executable programs. Since the ACL2 language has a formally defined semantics, specifications and programs are amenable to formal proofs. In particular, specifications that are easy to reason about and to validate against external requirements can be provably refined to efficient executable code. Kestrel Institute's APT toolkit of automated program transformations, built on top of ACL2, allows a developer to synthesize efficiently executable implementations from high-level declarative specifications, automatically generating formal proofs of the correctness of the implementations with respect to the specifications.

Benefits and Possible Extensions of this Work

Collaboration Opportunities

Please contact us if you would like to explore collaboration ideas with us, or if you would like to sponsor related research.