Runtime Verification April 2023 Updates
Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of April. 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 April, we wrapped up another audit with our long-time client, Blockswap. This time around, the audit focused on their Proof of Neutrality code. A technical report has been published, and a blog post will be coming up in the upcoming weeks. We have completed several other audits and we will be announcing them soon on our Twitter account.
EVENTS
For this month, we have two minor updates regarding events. While Aellison, one of our formal verification engineers, attended EthRio and EthSamba earlier this month, Denisa gave a talk at the Logic Seminars by ILDS about “A General Framework for Reasoning About Faulty Distributed Systems II”.
K-FOUNDRY
These are the monthly updates from our team working on K-Foundry:
- KEVM Foundry integration now supports bounded model checking mode. This is what you are familiar with if you’ve used tools like Halmos or Certora, which do not require you to write loop invariants! If you have used KEVM, but do not feel like writing loop invariants, you can now use option ` — bmc-depth N` to specify that you want to do bounded-model-checking instead of full verification.
- The KEVM Foundry integration has seen some significant improvements. In addition to many bug fixes, reasoning lemmas have been added, which should speed up symbolic execution and improve prover-time. The user interface allowing KCFG visualization is much smoother and should not crash anymore, and provides more informative output about the Solidity code being verified, including a source-map showing where in the Solidity code execution you currently are (instead of just displaying bytecode level information).
K- FRAMEWORK
We also bring some updates regarding our K efforts:
- The Java backend has been removed from the code repo. From now on, Symbolic execution will be handled exclusively by the Haskell backend.
- The BMC (bounded model checking) functionality of K has been overhauled and integrated into the pyk library for better control and future support.
- The bison parser can now be generated as a library. More details can be found here.
- Minor or incremental improvements to error messages and graceful failure:
- KLSP completion: don’t insert whitespaces around parens.
- Improved documentation and updated dependencies version.
- New chapter added to the K tutorial 2_lesson/01_macros.
ERCx
If you are a token investor, April was your month on ERC X ercx.runtimeverification.com. We have an updated homepage that takes you straight where you need to go.
After evaluating the tokens, you can bookmark your favorite ones and organize them in custom lists. Save everything to your account by using a GitHub or a Google login.
You’ll see the latest generated report for each token, but you can always create a new one.
If you are a developer, we have more tests for ERC-20, and we’ve already started working on the test suite for ERC-4626. Each report comes with more details about the tests we run.
As always, we welcome your feedback on the website or through our Discord server.
That’s all for this month’s updates. Stay tuned and join us in Discord to not miss any news from us.
