Runtime Verification October 2023 Updates

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

This time, we are bringing a lot of updates to our events section. Let’s start first with what our team has been up to this past month:

• Grigore Rosu presented “Pi²” at xDay in Bucharest. Recording available on YouTube.
• Virgil Serbanuta presented a Kasmer prototype ( property verification for MultiversX) at xDay.
• Xiaohong Chen presented at OOPSLA. The presentation explained how combining K and matching logic can reduce the trust base of language-agnostic FV from 120k lines of Haskell to a 200-line proof checker.
• Palina and Jin held a workshop on K and Kontrol at the International Symposium on Automated Technology for Verification and Analysis (ATVA, 2023) in Singapore, with materials and exercises available in the repository: https://github.com/runtimeverification/k-tutorial-atva-2023.
• Our team in the Bucharest office organized a one-day workshop to discuss different topics, including the state of K, Kontrol, Kasmer, Matching Logic in Lean and Proof of Proof with Pi. All videos are available on YouTube.
• Daniel presented a talk about FM, Rust, and KMIR at the Rust Brisbane meetup.

And to continue, we want to announce that our team will be at DevConnect in Istambul later this month. The team will speak at different events organized by the community about different topics. Here is where you can find them:

• Grigore Rosu will speak at AltLayer Rollup Frontier Day about “Pi²”
• Raoul Schaffranek will speak at EVM Summit about “The Symbolic Solidity Debugger”
• Gigore Rosu will participate in a panel discussion at the Nethermind Summit
• Yliès Falcone will speak at TrustX about “What Did I Learn by Testing ERC-20 Tokens at Large?”
• Raoul Schaffranek will speak at TrustX about “The Symbolic Solidity Debugger”

BLOG POSTS

If you want to know more about ERCx or you have never heard of it, we have you covered. This past month, we published three different articles diving into different areas of our new tool:

• “Towards a Comprehensive ERC Test Suite” provides an intermediate report to the community on ERCx’s mission of providing the community with handcrafted, comprehensive, and complete test suites for the most used ERC standards.
• “Is my ERC-4626 vault token up to the standard?” explains how our ERC-4626 test suite works and how you can get started to make sure a contract complies with the standard requirements.
• “Testing ERC-20 Tokens Part 1: An Arsenal for Bug Detection” is a blog we published in partnership with Certora and compares different test suites and bug-finding tools for ERC-20 tokens.

AUDITS

During October, we published different reports and blog posts from audits completed in the past. For Zivoe we conducted an audit on the Core and Locker contracts and published two different reports and a blog post summarizing the audit. The other audit we announced was the Blockswap’s Stakehouse Withdrawals audit, and we published a technical report with all the details and findings.

KONTROL (PREV. K-FOUNDRY)

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

• Updated documentation for Kontrol with up-to-date installation and usage instructions at https://docs.runtimeverification.com/kontrol.
• Continued the work on factoring out Kontrol — the K- and KEVM-based tool for Foundry projects verification — to a separate tool and repository; for example, the foundry.md file containing semantics of Kontrol and Foundry cheatcodes has been moved to Kontrol, making it easier to support new cheatcodes.
• Aligned the test selection functionality in `kontrol prove` with that of `forge test`: now, to choose the test(s) to be analyzed, run `kontrol prove — match-test ContractName.methodName` — this command will initiate verification of all functions in ContractName that match the `methodName` regular expression.
• Enabled infinite gas to be used in `kontrol prove` by default, while fixed amount of gas in a test can be provided via `kevm.setGas(uint256)` cheatcode.
• `KontrolCheats` contract specifying the interface for Kontrol cheatcodes is now available as an easy-to-use Foundry library: https://github.com/runtimeverification/kontrol-cheatcodes/, which can be installed via `forge install runtimeverification/kontrol-cheatcodes`.
• Added support for the execution of smart contract initialization code, providing the ability to include test’s constructor into the execution via ` — run-constructor` option in `kontrol prove`.
• Made simplification of the initial state’s KCFG default in `kontrol prove`.
• Added `kontrol version` command, which shows the currently installed version of Kontrol.
• Added the ability to specify the Solidity compiler (`solc`) version to be installed with Kontrol via `kup`: for example, to automatically install `solc` v0.8.13 with Kontrol, run `kup install kontrol.solc_0_8_13`.

K FRAMEWORK

We also bring some updates regarding our K efforts:

• Improvements to K packaging and installation for end users:
  - Big improvements to kup’s first-touch installation process; the size of a K installation is now much smaller and makes better use of binary caches.
  - ARM64 Macs are now fully supported for K development.
  - We have streamlined the set of platforms for which we ship packaged releases, in order to provide better support for our core set of Ubuntu Jammy, macOS and kup.
• Substantial performance improvements for semantics that rely on C-like (array-of-bytes) memory models via new internal data structures and hooks.

ERCx

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

• We improved our ERC-20 and ERC-4626 test suites by adding more tests, improving some of the tests, and reclassifying some tests.
• Version 0.8.0 of our VS Code plugin is available. Our plugin lets you run tests individually and per level (minimal, recommended, desirable, …).
• We added pages listing all top tokens from Etherscan and Uniswap letting you see how those tokens stand with respect to our test suite.
• We worked hard to crank two test suites for ERC-721 and ERC-1155. These will be made available next month. Stay tuned!

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