David J. Pearce (Blog)

Formalising the Ethereum Virtual Machine in Dafny

Monday, February 6th, 2023

Since starting at ConsenSys, the main project I have been involved with is a formalisation of the Ethereum Virtual Machine in Dafny called the “DafnyEVM”. Our goals share some similarity with Runtime Verification’s KEVM project.

Disassembling EVM Bytecode (the Basics)

Wednesday, January 4th, 2023

Recently, I’ve been looking at how to disassemble (and eventually decompile) bytecode for the Ethereum Virtual Machine (EVM). This is an interesting computer science problem which I’ve been thinking about lately.

Formal Verification of a Token Contract

Thursday, September 15th, 2022

Following on from my previous post on verifying an auction contract in Whiley, I thought it might be useful to look at a more challenging example. A token contract is a very common form of smart contract which allows someone to create and manage their own currency.

Formalising a Simple Virtual Machine

Tuesday, June 28th, 2022

Since starting my new role at ConsenSys, I have become interested in formalising virtual machines. For example, there are already some formalisations of the Ethereum Virtual Machine (e.g. in K, Lem, Coq).

Type Checking in Whiley goes Both Ways!

Wednesday, June 15th, 2022

Type checking in Whiley is a curious thing as it goes both forwards and backwards. This is sometimes referred to as bidirectional type checking (see e.g. here and here). This is surprisingly useful in Whiley (perhaps because the language has a reasonably unusual feature set).

Whiley gets Rusty!

Tuesday, May 31st, 2022

I’ve been learning Rust for a while now but, at the same time, trying to continue developing Whiley. Since Whiley was written entirely in Java, these activities were mutually exclusive and it was frustrating trying to balance things!

Verifying an Auction Contract in Whiley

Tuesday, May 17th, 2022

Since Whiley is a general purpose verification system, I thought it might be interesting to try and verify a smart contract. Smart contracts are well suited to formal verification tools (like Whiley), as they are small and typically self-contained.

Puzzling Strong Updates in Rust

Wednesday, April 27th, 2022

The idea of a strong update comes from earlier work on static analysis and, in particular, pointer analysis. To understand this, let’s imagine a hypothetical non-null analysis for C: int* r = (int*) malloc(sizeof(int)); int** p = &r; At this point, our non-null analysis would conclude that p was nonnull and that r was nullable.

Modelling Borrow Checking in Rust

Monday, December 6th, 2021

Recently, I’ve been working on a formalisation of borrow checking in Rust. The idea is to help people think clearly about how borrow checking works (in someways perhaps similar to the Stacked Borrows work but with a different perspective).

Verifying the Whiley Standard Library

Wednesday, October 27th, 2021

For sometime now, its been possible to use Boogie / Z3 as a backend for verifying Whiley programs. Initially that was pretty sketchy, but it’s really starting to ramp up now.

1
2
3
4
5