Runtime Verification July 2023 Updates

3 min readAug 3, 2023

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of July. 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 July, we wrapped up several audits, including Zorp’s Eden zkVM design audit. For Zorp’s design audit, a technical report and a blog post has been published detailing what went down during the audit. Future announcements about finished audits will be made on our Twitter account.

EVENTS

A big part of our team traveled to Paris to enjoy EthCC and all the events organized by the community (and some croissants in between events). Here is a recap of all the speaking engagements our team participated in:

Yliès gave a presentation at EthCC about “ERCx, Fast Checking of ERC standards and Beyond,” and the recording can be viewed on youtube.
Two members of our team participated in DeFi Security Summit. First, Palina gave a talk, “Towards Adoption of Symbolic Execution for DeFi Security”, about existing symbolic execution tools for smart contracts as well as practical advice on how to make these tools work better. Our CEO, Grigore Rosu, also participated in the event as one of the panelists of the Formal Verification panel. Both videos can be found on youtube, Palina’s presentation and Grigore’s panel discussion.
Our client and friend, Blockswap, organized Multichain ERC20, in which Juan participated giving a talk, Security™: Auditing / Formal Methods, about the difference between formal verification and traditional code auditing and Runtime Verification’s unique approach to formal verification methods. He also participated in a Fireside chat about Order Flow Auctions and Credible Commitments. Recordings of the talk and fireside are also available on youtube.
Last but not least, Grigore Rosu also gave a presentation about QED: Universal Proof Systems. ZK for AI/ML & Blockchain at OFR Paris, organized by one of our investors, IOSG. The recording is already available on youtube.

KONTROL (K-FOUNDRY).

These are the monthly updates from our team working on Kontrol:

A rebranding has been carried out. From now on, Kontrol will be the new name for K-Foundry.
Integrated a new booster backend, significantly speeding up symbolic execution of Foundry tests. The booster backend is enabled via the ` — use-booster` option available in `kevm foundry-prove`.
Added ` — counterexample-information` option to `kevm foundry-prove`, which shows counterexamples for failed Foundry tests. The output, then, contains the concrete values that symbolic variables should take for the test to fail.
Removed performance bottleneck from unnecessary disk I/O by splitting KCFG representation on disk into a multi-file structure.

K- FRAMEWORK

We also bring some updates regarding our K efforts:

Fixed a performance issue related to JSON file serialization in the kompiler part.
Started integrating the booster backend directly into the K framework repo. This should make it easier to have a faster symbolic execution engine in the future.
Added a Python implementation of the K outer parser to pyk.
Several important bug fixes to the new booster backend, enabling it to handle more real-world proofs.
Garbage collection support for the recently added range map type in the llvm backend.

ERCx

And, before wrapping up this month’s newsletter, here are the ERCx updates:

Added a REST API. You can now get all the good stuff of ERCx automated from any programming language and start building your own services.
Released an ABI generator. Our generator gives you the JSON representation of the ABI of a token.
Introduced checks on the submitted code source of tokens and clarified the requirements to help developers test their source code.
A new IDE will be coming soon.
Improved the design of the report of tokens to make them more readable.

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