Runtime Verification November 2023 Updates

4 min readDec 4, 2023

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of November. 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.

EVENTS

The month of November has been a busy one attending and speaking at events, so let’s get into all the events our team took part in:

Palina Tomach had the pleasure of joining Patrick Collins on the Cyfrin Audits YouTube channel to talk about Formal Verification and Kontrol.

A part of our team traveled to Istambul to attend DevConnect and speak at some of the events organized by the community, including TrustX, EVM Summit, Alt Layer Frontier Day and Nethermind Summit. Last week, we published a blog post with our participation in those events and a summary of the topics and we also published a Twitter thread with a shorter version of the blog.

Rikard Hjort attended the Urbit Assembly in Lisbon and moderated a panel discussion on how to make Urbit secure and what a secure Urbit looks like. Panel participants included Urbit experts Logan Allen, and Joe Bryan and cybersecurity expert Ryan Lackey. Rikard also presented our work on %quiz at Urbit Demo Day

Ylies Falcone joined the BeerFi meetup in Prague to share with the audience about ERCx. No recording is available for this talk but you can check our other ERCx talks and resources.

BLOG POSTS

In November, we published a new blog post announcing KMIR, a concrete and symbolic execution of Rust MIR. The blog shows a tutorial on how to extract MIR from the Rust compilation process and how to execute MIR programs with KMIR. We also would like to thank The Web3 Foundation again for the grant received to develop the syntax and semantics of Rust MIR.

KONTROL

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

Added ` — no-forge-build` option that helps skip the `forge build` step in `kontrol build` and use pre-compiled artifacts instead — this way, the user can call `forge build` with options they need prior to `kontrol build`.
Improved help messages and support for backend- and SMT-related options in Kontrol. `kontrol prove`, `kontrol simplify-node`, `kontrol step-node`, `kontol section-edge`, and `kontrol get-model` commands now all have access to options that help customize the interaction with the backend RPC server and the SMT solver, such as ` — use-booster`, ` — kore-rpc-command`, ` — trace-rewrites`, ` — port`, ` — maude-port`, ` — bug-report`, ` — smt-timeout`, ` — smt-retry-limit`, ` — smt-tactic`. Detailed information on these options is available via `kontrol — help`.
Improved Kontrol source files organization by moving cheatcode definitions to a separate file cheatcodes.md.
Improved handling of the `expectRevert` cheatcode, which helps ensure that the function call reverted during its execution.
Added the `.` symbol to the list of characters being escaped in contract names during `kontrol build` — now, smart contracts containing `.` in their names can be kompiled successfully for further verification with Kontrol.
Fixed a bug with `block.number` value not being carried over from `setUp()` function — now, the value set via the `vm.roll(uint256)` cheatcode in `setUp()` is respected in the following tests.

K FRAMEWORK

We also bring some updates regarding our K efforts:

Released K v6.1.0. This contains cumulated changes over the past five months where we continued to improve the performance of the kompiler and the prover. We also updated dependencies that allowed us to bring native support to Apple Silicon. As a result, we dropped support for Ubuntu 20.04 Focal and we will change our focus to the upcoming release of Ubuntu 24.04. We strive to provide support for the last two LTS of the major platforms.

ERCx

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

Some features and parts of the token reports now require creating an account.
Added tests for the ERC-4626 vault tokens and updated of our VS Code plugin to support them.
Revamped token reports for a better experience.

That’s all for this month’s updates. Stay tuned and join us on Discord so you don’t miss any news from us.