The Dafny-Clojure interop stays at the namespace boundary: compile externally, call via Java interop. The developer experience requires knowing Dafny's name-mangling conventions (Foo_Compile.__default.myMethod for a named module, or _System.__default.myMethod for the top-level module) and managing a separate build step.

defverified is a macro that moves the boundary inside the .clj file:

(defverified sum-list [xs]
  {:requires [(all-ints? xs)]
   :ensures  [(== % (apply + xs))]}
  "method Sum(s: seq<int>) returns (r: int)
   requires forall i :: 0 <= i < |s| ==> s[i] >= 0
   ensures r == Sum(s)
   { r := 0; for i := 0 to |s| { r := r + s[i]; } }")

1. Latency: Dafny verification takes seconds to minutes. Acceptable at compile time, not at REPL eval time.
2. Error propagation: Dafny's verification failures must map to Clojure compile errors with useful source locations.
3. Naming: The macro must generate deterministic Java class names from the Clojure var name.
4. Caching: Recompile only when the Dafny source string changes (content-addressed).

defverified macro
  1. Hash the Dafny source string
  2. Check cache (~/.dafny-cache/<hash>.jar)
  3. If miss: write temp .dfy, invoke dafny build --target:java, compile to JAR
  4. Add JAR to classpath (dynamic classloader)
  5. Generate wrapper fn with spec checks from :requires/:ensures
  6. Return the wrapped fn

• Dafny-Clojure JVM Interop (the boundary this macro hides)
• Dafny spec transpiler (generates the spec checks this macro uses)