# Simbolik

<figure><img src="/files/zyyD4MaddMuRZ0Af4Fcs" alt=""><figcaption></figcaption></figure>

Simbolik is a free [Solidity](https://docs.soliditylang.org/) 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](https://marketplace.visualstudio.com/items?itemName=RuntimeVerification.simbolik).

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](https://simbolik.runtimeverification.com/#contact) 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.

{% hint style="warning" %}
Documentation will be provided here as soon as it is available.
{% endhint %}


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/simbolik/overview/readme.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.