Runtime Verification March 2023 Updates
Welcome to another issue of our monthly newsletter on Medium. This time around we bring our updates for the month of March. 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.
ERC X
Today we are soft launching ERC X http://ercx.runtimeverification.com, a tool designed to help token investors identify and avoid scams. It also helps developers write contracts confidently by evaluating each token’s technical quality.
We check for conformance to standards and desirable properties before and after deployment on MainNet. For ERC-20, we check properties of state variables, behaviors of transfers and approvals, contract balance, expected event emissions, and usage of the zero address.
We welcome your feedback here, on the website https://ercx.runtimeverification.com/contact, or our Discord server https://discord.gg/xaU4XmzUt7
BLOG POSTS
A new blog post has been published announcing KAVM and, with that, bringing Formal Verification to Algorand. The blog post covers the announcement of the public beta of KAVM, which is the formal semantics of the Algorand Virtual Machine built with the K framework. The blog also covers a small tutorial on how to get started and how to use it.
AUDITS
Last year we audited Gyroscope Protocol’s Mathematical Model Implementation but the audit results were kept private until this month. A week ago, we published the full report of the audit and a blog post explaining the details of what went down.
EVENTS
Our team worked with the Institute for Logic and Data Science to host 2 days of blockchain workshops in Bucharest covering an array of topics such as security, Zero-knowledge proofs, formal verification and tooling to name a few. All video recordings are already available on our youtube channel.
K-FOUNDRY
These are the monthly updates from our team working on K-Foundry:
- EVM-Semantics updated to support the MERGE(/PARIS) schedule, passing the Ethereum conformance test suite (v11).
- Working on materials to get everyone started using K-Foundry.
K- FRAMEWORK
We also bring some updates regarding our K efforts:
- Tagged a new minor release: v5.6.0 https://github.com/runtimeverification/k/issues/3260
- Updated tutorial examples to use the more modern backends.
- Improved debugging support for macs via lldb
- The K VSCode extension can now be found on Open-VSX as well https://open-vsx.org/extension/RuntimeVerification/k-vscode You can now install it in VSCodium directly from the IDE.
MONITORING
For this month, we are also introducing the updates from our monitoring team:
- Development of Liquidbot, a Keeper on AlgoFi designed to identify under-collateralized loans and clean up accounts that may negatively impact the protocol.
- We are working with the Hatom team on a Keeper that will launch when the protocol moves to Mainnet later this spring.
That’s all for this month’s updates. Stay tuned and join us in Discord to not miss any news from us.
