Runtime Verification March 2023 Updates

Runtime Verification
3 min readApr 5, 2023

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.

The ERC X website as of April 2023

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:

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.

--

--

Runtime Verification

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.