February 2023 Updates — Runtime Verification

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

BLOG POSTS

A new blog post was published covering our GitHub Guidelines For Collaborative Coding. The blog post is an internal guide we developed and use to be as efficient as possible with our software development. We also want to mention the blog post Serokell published describing the first phase of our collaboration on optimizing the Haskell part of K framework.

EVENTS

Although this update may be more timely in the next newsletter, we couldn’t wait a whole month to share it. Our CEO, Grigore Rosu, and our CTO, Everett Hildenbrandt just cameback from attending ETHDenver and other side events organized by projects in the ecosystem. They have participated in a series of events as a speaker and panelist including the “Future Computing Research Workshop” by @DelendumV, STAY SAFU! Security Day by @IOSGVC, DeFi Formal Verification in Practice by @CertoraInc and Multichain ERC20 by @blockswap_team. We will be adding the recording links to the talks in next month’s issue.

K FOUNDRY

These are the monthly updates from our team working on K-Foundry:

• Updated documentation for the evm-semantics repository(README.md), including instructions to get new users started running kevm proofs(VERIFICATION.md) and Foundry testing(foundry.md).
• New functionalities have been added to the KEVM Foundry integration. The visualization tool has been improved and new commands have been added to the Foundry command such as `section-edge`, `step` and `simplify-node`. (not yet added to the documentation, but will be soon in foundry.md)

RESEARCH

Our research arm in the company has been busy working on different projects. These are some of the highlights for this month:

• New results achieved in the completeness and expressive power of matching logic. Some of the completeness results will be shared soon.
• Implementation of an end-to-end proof generation procedure for ERE (extended regular expressions). This means that for any valid ERE expression, we can automatically generate a matching logic proof for the validity and check it using the proof checker.
• Started looking into Metamath Zero, a next-generation proof checker of Metamath, and learning how it may help to improve the performance and trustworthiness of the current 240-line proof checker.

K FRAMEWORK

We also bring some updates regarding our K efforts:

• The K Language Server gets new features like: contextual code completion, goto definition, find occurrences, syntax error reporting, selection ranges.
• Some inconsistencies in the K tutorial have been fixed and the web rendering of the K code has been improved.

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