Runtime Verification September 2023 Updates

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

During September, our team attended and spoke at different events around the globe. Our SEA team attended ETHSingapore and some side events where one of our team members,Palina, gave a talk “Komprehensive Approach to Smart Contract Security” at the Old Friends Reunion organized by IOSG. In Chicago, the ERCx team introduced ERCx to the ETH Chicago community at their inaugural conference by giving a talk and a workshop. The workshop is available on our website and shows how to analyze reports, find bugs, and build services on top of our Open API. On the academic side, Denisa and Dafina, part of our Romanian team, gave the following talks:

• “Solving the Muddy Children Puzzle using the VLSM framework” at LATD 2023 in Tblisi, Georgia, by Denisa.
• “VLSM: A General Theory for Reasoning about Faulty Distributed Systems” at the University of Bucharest by Denisa.
• “Asynchronous Muddy Children Puzzle” at FROM 2023 in Bucharest, Romania by Dafina.

KONTROL (PREV. K-FOUNDRY)

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

• Kontrol — our tool for verification of Foundry projects — is now available in its own repository (https://github.com/runtimeverification/kontrol) and can be installed using `kup install kontrol`. Instead of `kevm foundry-kompile` and `kevm foundry-prove`, you can run `kontrol build` and `kontrol prove` to compile and prove the tests in your Foundry project, respectively.
• Documentation for Kontrol can be found at docs.runtimeverification.com/kontrol. Screenshots for the example section have been updated for the Kontrol updates, including updates to commands. Users can submit issues/typos to Github if found.
• We simplified the process of building KEVM and from source: it can now be done using a new `kevm-dist` command, which makes it easier to contribute to KEVM! The updated instructions are available in the KEVM repository: https://github.com/runtimeverification/evm-semantics#building-from-source.
• Improved version management for proofs in Kontrol. If several versions of the proof are available, a particular version can now be specified using the ` — version` flag, making it more convenient for users to inspect different versions of a smart contract’s KCFG. For example, to interactively inspect a KCFG of the first recorded version of a test, run: `kontrol show ContractName.testName — version 0`. To execute `kontrol prove` on the first version of a proof, you can run `kontrol prove — test ContractName.testName:0`.
• Integrated Shanghai Ethereum network upgrade to KEVM, bringing it up to date with the Mainnet.

K FRAMEWORK

Our focus for September was mostly on small bug fixes and improvements to our CI infrastructure, including:

• Integrating Bencher to better keep track of performance regressions or improvements in our development process: https://github.com/runtimeverification/k/pull/3611
• Switching to Cloudrepo for our maven artifacts to streamline the release process of K libraries.
• Fixing various bugs related to upgrades to newer versions of libraries and OS.
• Improving the help message of the command lines tools by adding hints about the required argument type: https://github.com/runtimeverification/k/pull/3638

URBIT GRANT

We completed the Urbit Foundation grant to integrate K and enable Hoon property testing. We launched a website at https://runtimeverification.com/partnerships/urbit and a blog post/tutorial is in the works.

ERCx

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

• We launched a test suite for ERC-4626 vaults. To learn more about tested properties, please refer to What’s being tested. As always, we would love to hear your feedback on improving our ERC-4626 test suite.
• We improved the design of individual Token Report pages with the Score by function group.
• Our ERCx VSCode extension is now live on the marketplace!
• We brought several improvements and optimizations to our ERC-20 test suite.
• Lastly, we introduced some rug pull and honeypot detectors for deployed tokens, e.g., SHARK TECH (SKT).

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