Loading...
Supporting developers, startups, and full-fledged companies building on Stellar and Soroban
© 2025 Stellar Development Foundation
Subscribe to the Newsletter
By Advanced Debugging for Soroban Contracts
This project delivers an IDE-integrated, AI-enabled debugger for Soroban smart contracts, based on deterministic WASM-level execution and precise modeling of Soroban’s runtime behavior. To achieve this, it combines improvements to Soroban’s execution semantics, development of a local testnet node with debugging capabilities, and implementation of developer-facing debugging tooling that integrates directly with standard development environments and enables LLM-driven assistance for interpreting execution results and debugging artifacts to help developers understand contract behavior and failures.
We will build on RV’s existing Soroban semantics developed in Komet, extended with detailed tracing of execution steps and Soroban-specific host interactions. These improvements directly benefit all tooling built on the same semantics, including Komet (https://komet.runtimeverification.com/), by increasing execution observability and strengthening fuzzing and formal verification workflows for Soroban smart contracts.
We will deliver a local testnet node with debugging capabilities based on the improved Soroban semantics. The backend executes Soroban smart contracts deterministically against realistic ledger and test configurations, producing step-by-step execution traces that include storage access, authorization checks, events, and resource budgeting. Deterministic and semantics-grounded, these execution results provide a reliable foundation for both low-level debugging and higher-level, user-friendly interpretation via LLMs.
A Debug Adapter Protocol (DAP) server will be implemented on top of the Soroban testnet node, exposing standard debugging operations, such as stepping, breakpoints, execution control, and state inspection, mapped directly to WASM-level Soroban execution. The DAP server allows integrating seamlessly with modern developer tools while preserving Soroban-specific behavior.
We will deliver IDE integrations for VS Code and Cursor that connect to the DAP server and provide a developer-facing Soroban debugging experience. Developers will be able to step through WASM bytecode, inspect contract and cross-contract calls, and observe Soroban host function interactions. The IDE integrations will also provide LLM-enabled assistance for interpreting execution behavior, presenting the AI-generated notes and summaries derived from completed execution traces alongside debugging output. This enables local debugging of Soroban contracts against realistic Stellar ledger and test setups, while improving developer productivity and reducing debugging and audit effort across the Soroban ecosystem.
$150.0K
RV has significant prior traction building advanced debugging and analysis tooling. Simbolik, a production-grade debugger for Solidity smart contracts, has over 7.1k downloads across IDE marketplaces as of January 30, 2026, and is currently in an active beta program with a growing user base. Public download counts are available via the official extension listings:
VS Code Marketplace:
https://marketplace.visualstudio.com/items?itemName=RuntimeVerification.simbolik
Open VSX Registry:
https://open-vsx.org/extension/RuntimeVerification/simbolik
Simbolik supports advanced debugging capabilities such as time-travel debugging, rich execution inspection, a wide range of cheatcodes, with full transaction-level debugging planned for an upcoming release. It is integrated with BuildBear, enabling transaction debugging in a sandbox environment: https://www.buildbear.io/docs/tutorials/simbolik-debugger.
The tool has also been organically mentioned and discussed on social media by developers and security researchers, reflecting real-world usage and interest in advanced smart-contract debugging workflows, for example:
We will directly leverage this experience when building debugging tooling for Soroban, extending our existing WebAssembly (WASM) semantics, as well as Soroban semantics and execution modeling implemented in Komet. Komet, our fuzzing and formal verification tool, is already being actively used by projects building on Stellar, including the following projects:
fxDAO https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/FxDAO.pdf
TokenOps: https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/TokenOps.pdf.
In addition to internal development, Komet has received external contributions from ecosystem users, demonstrating the engagement beyond RV, for example: https://github.com/runtimeverification/komet/pull/92.
This existing adoption demonstrates both demand for and trust in our Soroban-focused tooling, and provides a strong foundation for delivering a debugger that integrates naturally into the Soroban developer workflow.
In addition, we have extensive experience using AI-assisted internal tooling to support security review workflows. We maintain an internal LLM-powered audit assistance tool that combines static analysis results and structured program information to generate specifications and code summaries, helping auditors quickly understand codebases during onboarding and review. We use this tool across all audit engagements, including Soroban smart contract reviews. While it is not publicly available, the experience of building and operating this tool informs our approach to reliably integrating LLM-based interpretation on top of deterministic analysis outputs.
Deliverable 1 — Basic WASM-Level Tracing
The first deliverable is focused on extending RV’s existing semantics for Soroban used in Komet (https://github.com/runtimeverification/komet) to support basic deterministic, step-by-step execution tracing for Soroban smart contracts. This tranche is scoped to adding tracing hooks and trace data structures at the semantics level and validating them on a set of representative Soroban execution paths. This establishes the execution observability foundation on which the local testnet node and developer-facing debugging tooling will be built in subsequent tranches.
The work is structured into the following engineering tasks:
Design the trace format
Enrich Komet semantics with hooks to match on opcodes and host function calls
Define K-rules for extracting relevant state changes into a custom intermediate representation (IR)
Define K-rules to encode the IR into the trace format and write traces to disk
Testing, CI, and QA
How to measure completion:
Soroban semantics extended with tracing instrumentation for Soroban execution and available in the repository (https://github.com/runtimeverification/komet)
Demonstrated execution traces for representative Soroban contracts execution paths
Formal specification and documentation describing trace format
Budget: $30,000 USD equivalent in XLM
Deliverable 2 — Local Soroban Testnet Node
This deliverable focuses on packaging the traced Soroban semantics into a local Soroban testnet node suitable for interactive debugging workflows. Its backend will execute Soroban smart contracts at the WASM level against a provided test setup and emit rich execution traces reflecting actual Soroban runtime behavior, including host function invocations, storage reads and writes, authorization checks, event emission, and resource budgeting. This component bridges the gap between semantics-level tracing and developer-facing tooling by providing a concrete execution environment that faithfully mirrors Soroban’s runtime behavior.
The testnet node is based on a formal K-specification of the Stellar RPC protocol. Since K-specifications are executable, we ensure seamless integration with the Stellar CLI and existing tooling built on the same protocol. This makes it easy for developers to deploy and send transactions without the need to learn a new tool. To provide machine-level tracing, the Stellar RPC protocol is extended with custom debugging methods.
The work is structured into the following engineering tasks:
Implement domain model, encoders and decoders for Stellar RPC payloads
Implement K-rules to parse and serialize Stellar RPC payloads
K-semantics for block mining
K-semantics for handling sendTransaction
K-semantics for handling traceTransaction
Implement a persistent state solution (flat state database or state trie)
Implement K-rules to parse and serialize its internal state into a custom JSON snapshot format + RPC endpoints to expose the snapshots
Testing, CI, and QA
How to measure completion:
Local Soroban execution and tracing backend available in a dedicated repository (github.com/runtimeverification/komet-node)
Execution traces exposing Soroban-specific runtime interactions (host calls, storage, auth, events, budgeting) available
Internal documentation describing execution model
Budget: $45,000 USD equivalent in XLM. The estimated engineering cost for this deliverable is $60,000 USD. The initial tranche (Tranche #0, $15,000 USD) disbursed upon approval will be directed toward this milestone's development, covering the remaining $15,000.
Deliverable 3 — Basic Debug Adapter Protocol (DAP) Server
The Debug Adapter Protocol (DAP) is a widely used language-agnostic protocol that separates the debugging user interface from the execution backend. This tranche will deliver a Debug Adapter Protocol (DAP) server built on top of the Soroban execution and tracing backend. The DAP server will expose standard debugging operations, such as stepping, breakpoints, execution control, and state inspection, mapped onto WASM-level Soroban execution, and will serve as the integration layer for IDE-based debugging.
Each debugging session spawns a dedicated Debug Adapter Protocol (DAP) server process. The DAP server is architecturally divided into two components: a debugging backend and a debugging frontend.
The debugging backend is responsible for executing and tracing transactions on its own isolated debug testnet (developed in Tranche 2). Upon initialization, the IDE provides the server with compilation artifacts, DWARF metadata, deployment scripts, and transaction data. The backend executes the deployment scripts and the target transaction, producing a complete execution trace.
The debugging frontend acts as the intermediary between the IDE and the backend. It exposes the execution trace via standard DAP messages, manages breakpoints, enables navigation through the trace (e.g., stepping and stack inspection), and lifts low-level virtual machine states into Rust language constructs. Full semantic state lifting is explicitly out of scope for this proposal. Our focus is limited to mapping program counters to the corresponding source lines and columns.
This work includes the following engineering tasks:
Domain model, encoders, and decoders for DAP messages
Implement a lightweight Stellar RPC client library
Debug Backend: spawn new testnet, execute deployment scripts, trace transaction
Debug Frontend: breakpoint management, disassembly, memory references, source mapping
Testing, CI, and QA
How to measure completion:
Functional DAP server compatible with standard DAP clients
Ability to step through select WASM execution traces and inspect Soroban-specific VM state
Initial documentation describing the DAP interface and supported debugging operations
Budget: $30,000 USD equivalent in XLM
Deliverable 4 — IDE Integrations
Within Milestone 3, we will deliver IDE integrations of the debugger with VS Code and Cursor, built on top of the DAP server. These integrations will provide an end-to-end Soroban debugging experience, allowing developers to interactively debug smart contracts using familiar workflows.
The debugger will allow developers to step through WASM bytecode during Soroban contract execution, inspect contract and cross-contract calls, observe host function invocations, storage access, authorization checks, events, and resource usage, and debug locally using realistic Soroban ledger and test configurations. In addition, the IDE integrations will include LLM-generated annotations derived from the execution results alongside debugging output to help interpret contract behavior during debugging.
The IDE integrations will automate the full debugging workflow, including contract compilation, launching an isolated debug testnet, contract deployment, transaction submission, and execution tracing. When a developer initiates a debugging session, the contracts are automatically compiled using the Stellar CLI with all required compiler settings preconfigured (e.g., enabling DWARF output). The IDE integration then spawns the DAP server (Deliverable 3) and establishes communication by providing the deployment scripts, transaction data, and breakpoint definitions. Once initialized, developers can control execution by pausing and resuming transactions, managing breakpoints, and inspecting variables in real time.
Importantly, this approach requires no modifications to the Soroban or Stellar toolchain. It leverages existing Rust's compiler (rustc) support for emitting DWARF debug information for WebAssembly targets, configurable via standard Cargo profiles.
The work is structured into the following engineering tasks:
Bindings to Stellar CLI for compiling, signing, and sending tx
Lightweight WebSocket client to communicate with the DAP server
Testing, CI, QA
How to measure completion:
VS Code and Cursor extensions published to their respective marketplaces
The code is hosted in a new GitHub repository (github.com/stellar-debug-vscode)
Ability to attach the IDE debugger to a Soroban execution session via the DAP server
Interactive stepping, breakpoint handling, and state inspection validated in the IDE
LLM-generated notes on execution results available within the IDE
Budget: $22,500 USD equivalent in XLM
Deliverable 5 — Documentation and Testing
We will produce comprehensive public user documentation and testing artifacts to support adoption of the Soroban debugging tooling delivered as part of this project. We will test the debugging functionality using a select representative Soroban smart contract to validate correctness and stability of the execution tracing, DAP server, and IDE integrations.
How to measure completion:
A new repository (github.com/runtimeverification/komet-debug-server) will be created.
End-to-end Soroban debugging workflow validated using a representative smart contract
User testing completed
Public documentation and usage examples available
Budget: $7,500 USD equivalent in XLM
RV is a formal methods–driven security and tooling company specializing in complex, safety-critical software systems. Since 2018, we've been building developer and security tooling and providing security services across blockchain ecosystems, working with Stellar Development Foundation, Ethereum Foundation, and others.
This project's core team:
Burak Yalçınkaya – Research Engineer, https://www.linkedin.com/in/bbyalcinkayaBurak holds an M.Sc. in Computer Science from Chalmers University of Technology, where he specialized in executable formal semantics and fuzzing using the K framework. He is the primary maintainer of WASM semantics and the project lead behind Komet, and has extensive experience building execution and analysis tooling grounded in formal semantics.
Raoul Schaffranek – Head of Developer Tooling, https://www.linkedin.com/in/raoul-schaffranekRaoul studied Computer Science at RWTH Aachen University, where he earned both B.Sc. and M.Sc. degrees. His master’s thesis focused on compositional modeling and fully automated verification of distributed systems. Prior to joining RV, Raoul worked as a software engineer at graphodata AG. At RV, he leads developer tooling efforts, including Simbolik and related debugging and analysis infrastructure, and drives the design of human-centric verification tools.[
](https://www.linkedin.com/in/raoul-schaffranek)**Lisandra Silva – Formal Verification Engineer,** https://www.linkedin.com/in/lisandrasilvaLisandra holds an M.Sc. in Informatics Engineering from the University of Minho, with a focus on Formal Methods and Cryptography. During an internship at Oracle Labs, she worked on modeling and verification of distributed system protocols and developed a framework for proving liveness properties in Agda. At RV, Lisandra has worked on Simbolik, Kontrol, and multiple formal verification engagements, applying mathematical and logical reasoning to real-world systems.
Raoul
Lisandra Silva
Palina Tolmach
bbyalcinkaya
No other submissions.