Ethereum's Recursive Length Prefix in ACL2

Alessandro Coglio
(Kestrel Institute)

Recursive Length Prefix (RLP) is used to encode a wide variety of data in Ethereum, including transactions. The work described in this paper provides a formal specification of RLP encoding and a verified implementation of RLP decoding, developed in the ACL2 theorem prover. This work has led to improvements to the Ethereum documentation and additions to the Ethereum test suite.

In Grant Passmore and Ruben Gamboa: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2020), Worldwide, Planet Earth, May 28-29, 2020, Electronic Proceedings in Theoretical Computer Science 327, pp. 108–124.
Published: 29th September 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.327.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org