Dafny Verified Effects Bridge

Dafny distinguishes:

• function: pure, ghost-eligible, no heap access, used in specifications
• method: may have side effects, modifies clauses, heap allocation

Clojure has no enforced pure/impure boundary but uses conventions:

• Pure functions for transforms (the codec pipeline)
• core.async channels for concurrent effects
• component lifecycle for stateful services
• atom / ref for managed mutable state (STM)

The Dafny-Clojure interop focuses on pure codec functions. This note explores what happens when Dafny method contracts (modifies clauses, fresh allocations) cross the boundary into Clojure's effect management.

Dafny method:
  method Insert(s: set<int>, x: int) returns (r: set<int>)
    modifies this
    ensures r == s + {x}

Clojure caller:
  ;; Which pattern?
  (swap! state dafny-insert x)          ;; atom -- but Dafny's "modifies this" conflicts
  (>! ch (dafny-insert @state x))       ;; channel -- who owns the state?
  (component/start (->DafnyService))    ;; lifecycle -- how do modifies map to start/stop?

• Map modifies clauses to Clojure's ownership model
• Define when Dafny method output can safely enter swap!
• Define when function output is safe for core.async pipelines
• Out of scope: distributed state, Dafny's concurrent verification

• Dafny-Clojure JVM Interop (parent article, pure functions only)
• Reversible pipeline transforms (effect-free codec contract)