A Subtle Rust Bug

Here at Runtime Verification, we are spending time developing and improving tools for the K Framework. In particular, one of the projects I have been working on is a new execution engine for concrete execution of programs in K semantics, which compiles to LLVM.

Because we compile to LLVM, we are able to make use of code in any programming language that targets LLVM. In particular, we use Rust for the portion of the runtime which handles operations over lists, maps, and sets.

Yesterday I discovered a very subtle bug in our Rust code which was causing our tests to fail. It was affecting the hash algorithm we use for maps and sets, which in turn caused a map lookup operation to fail even though the key it was supposed to look up was in fact in the map.

Continue reading

Formally Verifying Algorand: Reinforcing a Chain of Steel (Modeling and Safety)

Musab A. Alturki, Brandon Moore, Karl Palmskog and Lucas Pena

Earlier this year, Runtime Verification was engaged by Algorand to verify its consensus protocol. We are happy to report that the first part of the effort, namely modeling the protocol and proving its safety theorem, has been successfully completed. Specifically, we have used a proof assistant (Coq) to systematically identify assumptions under which the protocol is mathematically guaranteed to not fork.

Continue reading

Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

Ethereum 2.0 is coming. And rest assured, it will be formally specified and verified!

Ethereum 2.0 is a new sharded PoS protocol that, at its early stage (called Phase 0), lives in parallel with the existing PoW chain (called Eth1 chain). While the Eth1 chain is powered by miners, the new PoS chain (called Beacon chain) will be driven by validators.

Continue reading