VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education

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

system and claims

VeGo embeds deductive specifications in ordinary Go comments beginning //@. The resulting file remains valid Go, while the vegop engine extracts contracts, builds verification conditions, and solves them. The paper’s abstract lists contracts, loop invariants and integer variants, recursive measures, block-scope invariants, and equational chains with primed variables. It says, “Because specifications reside in comments, every VeGo file remains 100% valid Go source code that compiles and executes natively using standard Go toolchains” (section 1, p. 2).

The paper targets education and reports a native Go pipeline: comment preprocessing, control-flow graph and Static Single Assignment (SSA) transformation, weakest-precondition generation, and an HM[X] constraint solver with Fourier–Motzkin linear arithmetic (section 5, p. 8). It claims all algorithms and data structures in its CLRS, Kleinberg–Tardos, Okasaki, and Knuth suites verify 100% under vegop --strict (section 6.3, p. 12). This is the paper’s benchmark claim; the paper does not provide an independent proof of its tool implementation.

technique 1: inline Hoare contracts and named returns

What it is. Functions carry //@ Requires, //@ Ensures, and //@ Exsures annotations. Go named return values let postconditions refer directly to outputs. The paper’s Divide example requires n >= 0 ^ d > 0, returns (q, r), and ensures n = d*q + r ^ 0 <= r ^ r < d (section 4.3, pp. 6–7).

How to do it.

1. Write a precondition describing permitted inputs (section 4.3, p. 6).
2. Use named return values when postconditions need output identifiers (section 4.3, p. 6).
3. State the postcondition after the function body (section 4.3, p. 6).
4. Add Exsures when a state is impossible on function completion; VeGo checks it by assuming the expression and deriving contradiction (section 4.3, p. 6).

Verus form. Inference: map Requires to requires and Ensures to ensures on a Rust function. Inference: Rust return tuples can be named through a postcondition over the returned value, but VeGo’s direct named-return syntax does not carry over. Inference: encode impossible states as a proved lemma or postcondition contradiction; Verus has no VeGo Exsures annotation.

Evidence and limits. The Divide example’s invariant maintains n = d*q + r and 0 <= r, while the variant proves decreasing non-negative remainder (section 4.3, p. 6). The paper’s pedagogical examples assume integer arithmetic and do not establish floating-point or unsafe-pointer semantics.

technique 2: loop invariants, variants, and inductive predicates

What it is. Every loop receives an //@ Invariant and an integer //@ Variant that is non-negative and strictly decreases. The paper states, “Loops require an //@ Invariant and an integer //@ Variant termination measure (bounded below by 0 and strictly decreasing on each iteration).” (section 4.4, p. 7). The SumLoop example defines an inductive sumTo(A,i,s) predicate: at i<=0, s=0; otherwise there exists a prior sum t with sumTo(A,i-1,t) and s=t+A[i-1] (section 4.4, pp. 6–7).

How to do it.

1. Define a predicate capturing the partial result after an iteration (section 4.4, p. 7).
2. State bounds and the predicate as the loop invariant (section 4.4, p. 7).
3. State a variant such as 0 <= (|A|-i') = (|A|-i-1) < (|A|-i) (section 4.4, p. 7).
4. Prove initialization, preservation through the body, and exit implication to the postcondition; these are the verification conditions generated by the pipeline (section 5, p. 8).

Verus form. Inference: use invariant clauses on while/for loops with a decreases clause for termination, and define a spec fn predicate for the recursive sum relation. Inference: VeGo’s primed update notation is not Verus syntax; express the post-state relation through the loop invariant and ordinary assignment semantics.

The paper also verifies recursive SumRec using //@ Measure |A|-i and an inductive sumRecPred over [i,|A|) (section 4.5, p. 7). Inference: use a Verus decreases expression and a recursive spec fn/lemma to establish the same well-founded measure.

technique 3: primed relational state and SSA mapping

What it is. VeGo uses unprimed identifiers for pre-state values and primed identifiers for values after a statement or loop iteration. For x := 0; x = x + 1; x = x + 2, it records x=0, x'=1, and x''=3; each prime maps one-to-one to an SSA version (section 4.2, pp. 5–6). At a loop back-edge, the updated prime is reconstituted as the next iteration’s unprimed state.

How to do it.

1. Identify pre-state values with unprimed names (section 4.2, p. 5).
2. Use one prime for each sequential mutation within a statement block (section 4.2, p. 5).
3. State relational array properties such as A'[i] = 2*A[i] and preservation for k != i (section 4.2, p. 6).
4. Map the relation to SSA versions and solve the resulting first-order constraints (section 4.2 and 5, pp. 6 and 8).

Verus form. Inference: use old(...) in postconditions for pre-state values and quantified sequence/map updates for mutated elements; do not write VeGo prime syntax in Verus. Inference: Verus’s old is a postcondition construct, whereas loop invariants describe the state at each iteration.

technique 4: block invariants and contract precision

What it is. //@ Preserves asserts a property across a nested block, such as preserving |A| while doubling every element (section 4.6, p. 7). VeGo also compares declared contracts with a principal pair: weakest precondition wp(C,Q) and strongest postcondition sp(P,C). This detects weak or vacuous contracts.

The sorting case study shows why. sorted(A) alone is satisfied by a function returning all zeros; adding multiset(A) == multiset(A') enforces permutation preservation (section 4.7, pp. 7–8). The paper states, “However, a function returning all zeros also satisfies sorted(A).” (section 4.7, p. 8).

How to do it.

1. State a block property with Preserves when control-flow scope must retain it (section 4.6, p. 7).
2. Compute or reason about the weakest precondition and strongest postcondition (section 4.7, p. 8).
3. Strengthen postconditions with relational properties such as permutation preservation when a weaker property admits bad implementations (section 4.7, p. 8).

Verus form. Inference: use a loop invariant or a lemma to preserve slice length; use sequence/multiset specifications to state permutation preservation. Inference: Verus does not expose VeGo’s automatic principal-contract checker, so contract adequacy requires explicit review and proofs.

technique 5: SSA and weakest-precondition verification pipeline

What it is. The architecture has four stages: extract and desugar comments and interval quantifiers; build a CFG and SSA versions; generate weakest-precondition verification conditions; solve them with native HM[X] and Fourier–Motzkin arithmetic (section 5, p. 8). The paper’s rationale is that SSA is mathematically equivalent to first-order functional programming, so imperative updates become equations over versions.

How to do it.

1. Parse annotations and desugar clopen intervals, slice-range quantifiers, guarded loops, and skip (section 5, p. 8).
2. Convert assignments to SSA versions x0,x1,... (section 5, p. 8).
3. Generate a VC for each execution path using weakest preconditions (section 5, p. 8).
4. Solve VCs with the native HM[X] constraint and Fourier–Motzkin solvers (section 5, p. 8).

Verus form. Inference: Verus performs its own verification-condition generation and SMT solving; a VL integration should preserve source-level requires, ensures, invariants, and decreases rather than attempting to reproduce VeGo’s parser. Inference: SSA is a useful mental model for explaining mutation, but Verus code should use valid Rust/Verus constructs.

technique 6: interactive verified-development workflow

What it is. Students create .vgos headers for external packages, write annotated .vgo files, receive LSP diagnostics, compile a gated entry point with runtime assertions and an internal verified variant, then transpile to ordinary .go for native testing (section 5.1, pp. 9–10).

How to do it.

1. Declare external function contracts in .vgos headers (section 5.1, p. 9).
2. Write Go plus Requires, Ensures, Invariant, and Measure comments (section 5.1, p. 9).
3. Use the VS Code LSP diagnostics to repair unproven invariants, bounds, and vacuous contracts (section 5.1, p. 9).
4. Compile with vegop compile or vegop compile-pkg, then run standard Go tests (section 5.1, p. 10).

Inference: for Verus, the analogous loop is editing Rust, running the project verifier, and using diagnostics before integration tests. Inference: runtime assertion wrappers can complement proofs, but must not replace proof checking for trusted internal calls.

evidence, assumptions, and VL threat

The paper reports 100% strict verification across its named textbook benchmark suites (section 6.3, p. 12), and describes three tree/heap encodings—compact arrays, sparse arrays, and boxed inductive nodes—with quantified heap predicates (section 6.1, pp. 10–11). It proposes concurrency specifications for goroutines and channels as future work (section 8, p. 13), so those claims are roadmap, not evaluated results.

The trusted base includes VeGo’s parser, SSA transformation, VC generator, HM[X]/Fourier–Motzkin solver, and specification annotations. Inference: a bug in any of these can invalidate a reported proof. Inference: the greatest threat to agent-written verified Rust is a vacuous or overly weak contract; VeGo’s sorting example demonstrates that proving sorted alone permits an incorrect implementation. VL should preserve the paper’s discipline of explicit invariants, termination measures, mutation relations, and permutation/data-preservation properties, while using only Verus constructs validated in its own reference.

techniques for the catalog

• inline contracts: place preconditions, postconditions, and impossible-state claims beside executable code
• invariant and measure proofs: combine loop invariants, decreasing variants, and inductive predicates
• primed-state reasoning: relate pre/post mutation states and map them to SSA versions
• contract precision: strengthen weak specifications with preservation and permutation properties
• SSA VC pipeline: desugar annotations, build SSA, generate weakest-precondition VCs, and solve constraints
• interactive workflow: use headers, editor diagnostics, verified compilation, and native tests as one loop

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15