Our team is already in Thailand, ready to take over DevCon and the side events organized by different teams in the ecosystem! In this blog, we list all the events where our team will be speaking, how to get in touch with us and meet us, and update you on the latest developments in our tooling.

Speaking at DevCon and Side Events

We are lucky and grateful to have been selected by several teams to share our work and expertise with the community! Our team will be attending many side events besides DevCon, but if you want to know more about our engineers and the work we currently do with our open-source tooling, make sure you catch up with us at some of the events where will be speaking.

DeFi Security Summit

Who doesn't love workshops? Make sure to join the two workshops that we are hosting at DeFi Security Summit about Simbolik and Kontrol:

Juan will speak November 7th at 13:30 about "Kontrol Unlocked: Foundry-based Formal Verification for 10x Devs and Auditors".

Raoul will seapk November 8th at 14:10 about Simbolik "Solidity under the hood"

Aggregation Summit

Before DevCon starts, you can also catch Aellison sharing about cross-chain security practices at Aggregation Summit next November 10th at 12:45 :

Consensys Diligence x Creed | Hackers with Hearts Bangkok

Palina will be part of the panel about fuzzing at the Hackers with Hearts event at 3pm, November 10th

DevCon

Two years ago in Colombia we had the pleasure of sharing with the community twice. This time around, we will have three sessions at the main event! These are the talks and times planned for DevCon:

Getting in Touch with Us

With so many people and side events, sometimes it can be a bit hard to run into someone. If you want to catch up with us at a side event, for a coffee, or even for a demo of our tooling, please contact Gregory (@gregorymakodzeba) or Paul (@paulstanlen) directly and they will connect you with one of our engineers.

Tooling Latest Updates

Kontrol

Since announcing the release of Kontrol v1.0 in August, the team has been hard at work on a number of improvements to help developers and auditors perform better verification of their smart contract code. We've made several optimizations, including introducing the option to disable stack overflow sanity checks for each executed opcode, and preventing unnecessary intermediate node simplifications in setup and constructor proofs. These enhancements combine to provide significant improvement in Kontrol's performance, resulting in faster verification of your Solidity smart contracts.

Another important area of improvement leverages the source mapping techniques employed by our Simbolik debugger, which efficiently maps a contract's EVM bytecode to the Solidity source code, effectively demystifying the bytecode and allowing Solidity developers to better understand formal verification results.

And finally, with the introduction of our support for Cancun we can now support new opcodes like MCOPY, as well as those that support transient storage, which should allow Kontrol to be used on new codebases that were previously unsupported.

Simbolik

The Simbolik team has been hard at work continuing to improve the tool over the past several months. As a reminder, Simbolik is Runtime Verification's Solidity debugger, designed for efficient debugging across EVM-compatible chains. It automates repetitive setup, allowing users to simulate interactions by deploying contracts and running scenarios with minimal manual intervention.

In support of the official release of Simbolik in August, we presented a workshop at the Web3 Security Summit entitled Solidity Debugging Meets Formal Verification, where we demonstrated extending the use of Simbolik to perform symbolic execution, as well as converting Solidity property tests into symbolic tests. The team also recently published a blog post on using Simbolik to streamline Solidity debugging and making these sessions reproducible and shareable, which makes identifying issues and performing audits simpler. This guide walks through debugging an automated market maker (AMM) contract, showcasing how digital actors simulate user behavior. Read the full post for an in-depth guide and practical examples here.

KaaS

Runtime Verification recently launched K as a Service (KaaS), a new cloud-based service making the power of K accessible to a broader user base by offloading the computational needs of formal methods to us through this cloud service offering. KaaS features include:

• Proof archiving, versioning and tagging, allowing users to maintain a history of their code over time.

• Proof collaboration, enabling developers and auditors to develop and prove their codebase as it evolves.

• Build configuration management for easy replication of proofs over time.

• Continuous Integration (CI) support for GitHub (default), with more coming soon.

• A CLI tool for easy integration into any CI test workflow. Run your proofs locally or in the cloud with kaas-cli.

• Remote Compute ensures users have all of the compute power and capabilities required to run K without the expense of maintaining hardware.

• Web interface for proof upload, download, archiving, and remote execution.

Check out the details on our KaaS Product Page, and find us at the DeFi Security Summit or Devcon for a full demonstration.

That's all for now. See you around Bangkok!