Runtime Verification June 2023 Updates

4 min readJul 3, 2023

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of June. As always, the updates that we post here are summarized and simple, but we are more than happy to give more details and answer any questions on our Discord server.

AUDITS

During June, we wrapped up several audits and published some long-awaited blog posts from past audits. For Ojo’s audit, a technical report and a blog post has been published detailing what went down during the audit. We also published Morpho’s AAVE v3 blog post. Back in 2022, we conducted an audit on Blockswap’s dETH Gateway, but only recently, the technical report and blog post were published. More announcements about finished audits will be made on our Twitter account.

BLOG POSTS

During June, we published two new blog posts related to products and development. The first blog post is the official launch announcement of our new tool ERCx. ERCx is a conformance and property-checking tool helping not only to check ERC-20 security properties but also with contract development. The second blog post published is the announcement of the new version of the K Framework. K v6 includes easy installation, IDE support, a Python API, RPC interface, Language Bindings, a Haskell backend & an LLVM backend, symbolic debugger capabilities, and faster symbolic execution.

EVENTS

Before we explain our plans for ETHCC week. Let’s take a look back to earlier in June when Bruce presented at PLDI (as part of the ACM FCRC conference in Orlando, FL) a tutorial aimed at graduate students interested in programming semantics, demonstrating how to get started using K, and the basics of what users can build with it.

For ETHCC, a part of the team is traveling to Paris from all over the world to attend the different events organized by the community. On top of that, we will be presenting at the following events:

16th July. Grigore Rosu will participate in a panel at DeFi Security Summit.
18th July. Grigore Rosu will give a presentation at OFR Paris — Generative World Architecture by IOSG VC.
19th July. Juan Conejero will give a talk at Multichain ERC20 by Blockswap Labs
20th July. Ylies Falcome will present “ERCx, Fast Checking of ERC standards and Beyond” at ETHCC.

K-FOUNDRY

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

KEVM now supports the latest hardfork SHANGHAI.
Updates to the usability of KEVM for raw K specs. Most people will want to write Foundry property tests, as they are easier, but raw K specs give you much more power! There were several features that were not exposed to users writing raw K specs, including proof saving/resumption and proof subgraph pruning, but now are!
When a KEVM proof (Foundry or raw K spec) fails, sometimes the prover runs off the rails and keeps trying to do the proof. This is tricky to detect when it happens, but we’ve improved the detection of this case so that it will report back quicker that the proof failed, making it easier to diagnose the problem.
Added support for a new KEVM cheatcode “freshWord” and “freshBool” which gives the ability to generate a symbolic variable in a Foundry Solidity test, which has much less overhead than the “symbolicStorage” cheatcode for a single value.
In addition, some simple bugs in how proof subgraph pruning worked are fixed, and that affects both Foundry users and raw K spec users.

K- FRAMEWORK

We also bring some updates regarding our K efforts:

Open-sourced the new booster backend. The new `kore-rpc-booster` is now open source, and being integrated into the K tools.
Added a new built-in type `RangeMap`, a map whose keys are stored as ranges, bounded inclusively below and exclusively above. Contiguous or overlapping ranges that map to the same value are merged into a single range.
Added ` — temp-dir` option to specify where to store all the temp files created at runtime. This can avoid some issues with accumulating files and read-only restrictions.
Added a new endpoint `get-model` to the RPC server, which tries to provide an example for a given configuration with constraints (important for counter-example generation).

ERCx

Before we list all the ERCx updates: most of the team will be in Paris for https://defisecuritysummit.org/ and https://www.ethcc.io/ (where we’ll demo the tool). Come talk to us on 7/20, 4:10 pm — Louvre Stage.

We added a new level of tests, AddOn tests. These tests check for properties of add-on functions commonly created and used by developers, such as increase and decreaseAllowance.
Support for the testing of contracts deployed on two testnets: Sepolia and Goerli; hence allowing developers to evaluate their deployed contracts.
Support for the testing of source code contract; hence allowing early debugging and testing of ERC-20 tokens.
A simplified and improved design of our website.

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