January 2023 Updates — Runtime Verification

3 min readFeb 2, 2023

Welcome to the first issue of our new updates section on our medium. In the past, we have used Revue to bring updates on what the team has been working on, but after they shut down the platform, we decided to move those updates to our social media and Medium profile.

The updates we will share from now on will be summarized and simple, but we are more than happy to give more details and answer any questions on our Discord server.

AUDITS

In the month of January, our team added three new reports to our GitHub Publication Repo. The first project, EUROe stablecoin, is built on Ethereum and is the first EU-based regulated stablecoin. World Mobile is the second project, a mobile network built on the Cardano blockchain aiming to bring connection even in remote places. And last but not least, we published the Ashswap report and blog post, a stable-swap protocol built on top of the MultiversX blockchain.

BLOG POSTS

One of our formal verification engineers, David Kretzmer, published a blog post in late December about Using Foundry to Explore Upgradeable Contracts (Part 1). Make sure also to check some of our older blog posts, such as “Foundry: Gen 2 of Ethereum Tooling”, part of our Foundry series and “Warning: Code Can Be Explosive”.

EVENTS

Last week “InFormal Workshop on Logics” took place. The event focused on formal specification and verification logics and was organized jointly by Runtime Verification (RV), the Institute for Logic and Data Science (ILDS) and the Research Center for Logic, Optimization and Security (LOS), University of Bucharest.

We will be posting the video recording this upcoming week on our youtube channel.

K FOUNDRY

These are the monthly updates from our team working on K Foundry:

KEVM now supports the most common cheatcodes used by Foundry property test suites: https://github.com/runtimeverification/evm-semantics/blob/master/include/kframework/foundry.md
A new visual interface for Foundry proofs has been added; more to come later.
Everett Hildenbrandt’s workshop recording about how to use Foundry for property test verification (hosted by Certora) is available on youtube.

RESEARCH

Our research arm in the company has been busy working on different projects. These are some of the highlights for this month:

Generating proof certificates for the K prover.
New results regarding the completeness of the matching logic proof system.
Certified checking of regular expression totality in matching logic.

K FRAMEWORK

We also bring some updates regarding our K efforts:

Work towards better IDE integration. Stay tuned to get announcements.
Many bug fixes to all components, making for smoother K experience.
A new tool called `kup` which allows for 1-line installation of K tools and many semantics. Adds preliminary support for Apple Silicon.
Release of new RPC-based prover in the pyk library , and work on an interactive visualizer for it.

K DEBUGGER

And for the K debugger tooling, which has been a major push for the K team:

We added experimental bindings in Python to LLVM-backend generated interpreters, which aid in building user-facing applications based on concrete execution.
We are running internal experiments on making language-specific debuggers on top of K, which can provide typical breakpoint style debugging that people are used to from other tools.

That’s all for this month's updates. Stay tuned and join us on Twitter to not miss any news from us.