Runtime Verification February 2024 Updates

4 min readMar 5, 2024

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of February. If you want to be up to date with what we are up to, follow us on X or join our Discord to get in touch with our team and ask them all your questions about our work and tooling.

EVENTS

Part of our team is currently in Denver, attending ETHDenver and all the side events organized around the main event. Grigore Rosu, our CEO, participated in a series of side events talking about Pi Squared and ZK technology. Those side events include Scale Summit (hosted by Nil Foundation and LambdaClass), Encode Club and StarkCity (hosted by StarkWare). Stay tuned to the next newsletter issue for the video recordings from the events we participated in.

BLOG POSTS

Our ERCx team has been working hard on shipping updates and writing a series of blog posts diving deep into the tool’s potential. This month, we published the second part of Testing ERC-20 Tokens: Advancing Benchmarking with Mutation Testing. Before looking at this blog, make sure to read the first part of this series: An Arsenal for Bug Detection.

AUDITS

Our team is working on reviewing code for various projects we will announce soon. One of our latest completed and published audits is the Synonym Finance protocol. As always, we have published a technical report and a blog post that can be viewed by anyone interested to know more about what went down during the audit.

KONTROL

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

To further facilitate verification of Solidity tests, we added support for function parameters of dynamic types in the calldata — such as `bytes` and `bytes[]` — as well as support for NatSpec comments that can be used to provide assumptions about the length of dynamically typed variables. For example, the following test can now be automatically verified by Kontrol:

```
    struct ComplexType {
        uint256 id;
        bytes content;
    }

    /// @custom:kontrol-length-equals content: 10000,
    /// @custom:kontrol-length-equals ba: 10,
    /// @custom:kontrol-length-equals ba[]:600,
    function test_complex_type(ComplexType calldata ctValues, bytes[] calldata ba) public {
        require (ba.length == 10, "DynamicTypes: invalid length for bytes[]");
        assert(ctValues.content.length == 10000);
        assert(ba[8].length == 600);
    }
```

The NatSpec comments labeled with the `@custom:kontrol-length-equals` tag indicate that `bytes content` is 10000 bytes long, while the `bytes[] calldata ba` array has 10 element, each 600 bytes long.

Added `kontrol refute-node` and `kontrol unrefute-node` commands. `kontrol refute-node` interrupts an invalid execution path so that it can be disproved later (via `kontrol unrefute-node`). This functionality lets the user control the exploration without having to restart execution. That way we, can identify invalid paths early and have the tool focus on the other ones for increased efficiency, while the user figures out what they need to do to ultimately remove those invalid paths completely.
Introduced a new Kontrol cheatcode: `kevm.freshBytes(uint256 length)`, which allows a user to generate a fresh symbolic bytes array of a given size, making Kontrol tests more expressive and flexible.
Updated the logic of verified test selection if no ` — match-test` is provided: now, `kontrol prove` would automatically verify all tests that are located in the `/out` folder of a Foundry project and start with `test`, `prove`, or `check` keywords.
Renamed the `kontrol summary` command to `kontrol load-state-diff`, which is our new feature that allows generating a summary for a Solidity function based on the list of account accesses that is generated by Foundry.
Implemented support for Foundry’s `mockCall` cheatcode — it now can be used in Kontrol tests to mock calls to an address with a particular call (and return) data: `function mockCall(address where, bytes calldata data, bytes calldata retdata) external;`.

K FRAMEWORK

We also bring some updates regarding our K efforts:

Focus on documenting and simplifying the behavior of the K language and compiler.
Many historic dark corners have been cleaned up to substantially improve the K tutorials and learning experience in a future release.

ERCx

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

Launched a test suite for ERC-721 tokens, aka NFTs! To know more about tested properties, please refer to our What’s being tested page.
Added Explorer and Uniswap Top Tokens from several Layer 2 chains.
Expanded 4626 Alliance Vaults to include vaults from several Layer 2 chains.
Added detectors for new ERC standards: ERC-165, 223, 721, 777, 1271, 1363, 1820, 2309, 2612, 2771, 2981, 4524, 4906, 5267, 5313, 5805 and 6372.
Based on the valuable feedback from our users, we simplified our test levels to the following four: Abi (Signature), Standard, Security, and Features.
Updated our VSCode extension to support the ERC721 test suite and the updated test levels.
As usual, we would love to hear your feedback on the above! In particular, please let us know which standard you want a test suite or a detector for.

That’s all for this month’s updates. Join us on X and Discord to never miss any updates from us.