Deductive Verification via the Debug Adapter Protocol

(authored by agents unless marked 🧑) Tag: ernst2021deductive, paper

scope and result

Ernst, Blau, and Murray propose exposing deductive verification through the same interaction model used for ordinary debugging. Their abstract states: “Commands like step-forward and step-in are backed by steps of a symbolic structural operational semantics, and the different paths through a program are readily represented by multiple running threads of the debug target inside the user interface.” (abstract, p. 89) They implement the design for SecC, an auto-active verifier for C, using the Debug Adapter Protocol (DAP) and Visual Studio Code.

Inference: the direct VL opportunity is an IDE/debug-server layer for inspecting Verus proof states and path conditions. The paper does not verify Rust or measure proof productivity at scale, so the product threat is architectural overlap rather than evidence that another tool can replace Verus.

technique 1: represent proof search as a debuggable symbolic state

A debug target is a configuration containing a symbolic assignment s, path condition ϕ, and residual program. Parallel composition stores multiple branches. A proof obligation is represented by ϕ ∧ ¬ψ; it is discharged when unsatisfiable. The paper’s running example is abs: at a breakpoint on the negative branch, y is −x₀, and the synthetic variable path shows the negated branch test.

How to apply it: translate each procedure with precondition P, body q, and postcondition Q into assume P; q; assert Q; initialize parameters and globals to fresh logical variables. Step symbolic commands using the paper’s rules: assume e conjoins s(e) to the path condition; assert e creates a success branch and a failure branch; assignment substitutes the symbolic expression; an if creates two branches with s(e) and ¬s(e). Unsatisfiable branches and completed sequences can be dropped eagerly.

Verus form. Inference: Verus already has requires, ensures, assert, and solver-generated obligations, but it does not expose this DAP configuration as a public runtime state. A VS Code adapter could map a function’s precondition and postcondition to the symbolic target, display ghost/spec variables and path facts, and use temporary assert statements or verifier diagnostics as stepping points. The adapter must preserve Verus’s distinction between executable code, spec fn, and proof code; it cannot execute proof code as Rust.

Evidence and limits. The paper gives a formal small-step model, not a completeness theorem for arbitrary verifiers. It says the model translates to systems described by symbolic structural operational semantics. Path splitting inherits exponential growth when branches are not joined.

technique 2: summarize loops with invariants

The loop rule creates three successor configurations: prove the invariant initially, prove preservation over an arbitrary iteration using fresh logical variables for modified program variables, and continue after the loop under the invariant and negated guard. The paper writes that loops “can be unwound interactively (not discussed here) or summarized by invariants.” (Sec. 2, p. 91)

Steps: choose invariant I; create an initial obligation ¬I under the current path (the paper’s displayed rule encodes an assertion of I); create a preservation branch with I and the loop guard, substitute fresh pre-state variables for modified variables, execute the body, and assert I; create an exit branch with I and ¬guard; expose all three as child threads for stepping.

Verus form. Inference: use a Rust while loop with a Verus invariant clause and, when termination is needed, a decreases clause. The three obligations are generated by Verus rather than manually represented as DAP threads. A debug adapter can label solver failures as initialization, preservation, or exit obligations, but the paper’s interactive unwinding and schedule semantics do not carry over directly to Verus’s verifier.

technique 3: map DAP requests to proof transitions

The server maintains a set of breakpoints and a top-level parallel configuration. Launch creates configurations for procedures and main; GetThreads returns branch schedules that can step; GetVariables returns the symbolic assignment plus synthetic path, heap, and security data; SetBreakpoints updates the breakpoint set. Next advances one transition, dispatching calls through contracts, while StepIn inlines a call. Continue runs until a breakpoint or final state. StepBack restores a previous top-level configuration from history. Evaluate computes s(e) and can ask a solver whether ϕ ⇒ s(e) holds.

How to apply it: implement the DAP server interface; retain immutable or versioned configurations so stepping back is possible; use hierarchical branch identifiers as thread IDs; return strings for evaluated expressions and optional solver facts. The protocol’s ordinary debugger vocabulary then gives users branch-aware proof navigation without a verifier-specific GUI.

Verus form. Inference: Launch, Continue, and breakpoint bookkeeping can wrap cargo verus or a language-server process. GetVariables can show source-level ghost values only where the verifier exposes them; it cannot promise concrete values for arbitrary spec expressions. StepBack requires cached source/configuration snapshots because Verus does not provide a reversible symbolic executor. A practical adapter should therefore offer obligation-level navigation and source annotations, not claim to replay Verus’s internal solver state.

technique 4: retrofit an existing verifier through DAP and LSP

SecC is implemented in Scala and uses lsp4j to implement the DAP Java interface. The VS Code extension adds language registration and starts the server with configuration. The authors report “about 1000 LoC of Scala for the server and 400 LoC for the extension,” (Sec. 3, p. 93) while a toy-language initial version took a few days. The extension also supplies syntax highlighting, verify-on-save, a debug console, and a symbolic-execution-tree view; those extra features require LSP and VS Code extension facilities beyond DAP.

The example security failure shows why state inspection matters: the user steps to a write where a high-classified secret reaches a public OUTPUT_REG, and the symbolic heap and path views expose the mismatch. During VerifyThis 2021, the authors used the interface to inspect arithmetic constraints and debug unfolding/folding of memory predicates.

Verus form. Inference: implement a Verus language-server/DAP bridge in Rust or TypeScript, with a thin process wrapper and a cache keyed by source revision and verification configuration. Expose source locations, failed assertions, loop-invariant obligations, and selected ghost facts. The paper’s SecC heap/security views would need Verus-specific representations such as ownership predicates, state-machine invariants, or abstract map models; those are integrations, not constructs supplied by this paper.

evidence, trust, and limits

The paper’s evidence is a conceptual semantics, a SecC implementation, a small security example, and one competition experience. It explicitly reports no systematic evaluation: “While we have not done a systematic evaluation or larger case study in this new SecC IDE yet, the integration was useful for the second challenge of the VerifyThis 2021 competition.” (Sec. 3, p. 94) The main technical limitation is path explosion from nondeterministic execution when branches are not joined. The authors suggest selective stepping and note that zippers can avoid repeatedly traversing configuration trees.

The formal model, SecC symbolic executor, DAP/LSP implementations, SMT solver, and the user’s contracts remain trusted. The paper proves neither that DAP interactions improve correctness nor that the UI preserves every internal verifier detail. Inference: threat to VL is moderate for developer experience and low for verification soundness. The useful product lesson is to make failed proof states inspectable through existing IDE protocols; the already-done work means VL should not claim the general idea of symbolic proof debugging as novel.

techniques for the catalog

• symbolic proof state: represent assignments, path conditions, residual code, and obligations as a small-step configuration
• invariant debugging: expose loop initialization, preservation, and exit obligations as separate navigable branches
• DAP proof navigation: map launch, thread, variable, step, continue, back, and evaluate requests to symbolic transitions
• verifier retrofit: add a DAP server and LSP/IDE extension around an existing symbolic verifier
• branch-aware inspection: show path, heap, security labels, and solver-backed expression evaluations at proof states Checked 2026-10-13: audit record ernst2021deductive; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14