Simbolik

A Symbolic Debugger for Solidity

Simbolik is a free Solidity debugger that allows developers to set breakpoints, step through the code, and inspect variables. It is conveniently available as a VSCode extension, so you can seamlessly integrate it into your development environment directly from the VSCode marketplace.

Simbolik's most distinguished feature is its symbolic execution mode, which allows its users to formally verify their smart contracts with unmatched precision and accuracy and an intuitive graphical user interface. Access to the symbolic execution mode is currently restricted; please reach out if you're interested.

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.