A Symbolic Debugger for Solidity
Simbolik is a symbolic debugger tailored for Solidity smart contract debugging. Leveraging the capabilities of the K framework, it employs symbolic execution techniques to meticulously identify potential vulnerabilities in your smart contracts. Conveniently available as a VSCode extension, you can seamlessly integrate it into your development environment directly from the VSCode marketplace.
VSCode extension is not published at this time, but as soon as it is this page will be updated with a link.

Why Create Simbolik?

At Runtime Verification our engineers and auditors noticed a lack of advanced Solidity debuggers, especially ones that combine the intuitiveness of classical interactive breakpoint-style debugging with the depth of symbolic execution.
To close this gap, we propose Simbolik, the “Symbolic Solidity Debugger.” Simbolik is a tool specifically designed to significantly lower the entry barrier for one of Computer Science’s most advanced quality assurance techniques.

What to Expect as a User

While we want to elevate our audience’s knowledge, we don’t expect any prior knowledge of formal methods or symbolic execution. We’ve opted into an intuitive user interface that merges seamlessly into VSCode, empowering developers to start with classical debugging and progressively harness symbolic features’ advanced bug-finding capabilities.

Benefits of using Simbolik

As you’d anticipate, Simbolik offers all conventional functionalities, from setting breakpoints to stepping through code (both at the Solidity and EVM levels), inspecting variables, and navigating call stacks.

What Sets Simbolik Apart

Simbolik can begin debugging with arbitrary symbolic storage and call data, allowing users to explore the comprehensive branching control flow graph and delve into the conditions assigned to each path. Essentially, debug a function once, and you’ve probed every potential behavior it could manifest.
Documentation will be provided here as soon as it is available.
Last modified 3mo ago