The Dafny-Clojure interop article covers the JVM boundary: Dafny compiles to Java, Clojure calls it. But Dafny's requires and ensures clauses are ghost-erased at compile time – the JAR carries no trace of the preconditions. If Clojure passes invalid data across the boundary, the "verified" code does not crash – it silently returns a result that violates the postcondition Dafny proved under its assumptions.

This note explores the inverse direction: parse .dfy source and generate clojure.spec.alpha definitions that enforce Dafny's contracts at runtime.

Dafny source     -->  JAR (ghost-erased)  -->  Clojure caller
  requires P(x)        (no P check)            passes x without P?
  ensures Q(r)         (no Q check)            trusts r blindly?

The spec transpiler closes this: requires P(x) becomes (s/def ::x P-spec).

• Parse requires, ensures, invariant clauses from .dfy files
• Generate clojure.spec.alpha or malli schemas
• Handle: numeric ranges, string predicates, sequence length, set membership
• Out of scope: quantifiers (forall, exists), ghost variables, heap predicates

1. Should the output be spec or malli? The interop article uses malli for the codec schemas.
2. How to handle Dafny's seq<char> vs Clojure's String – the type mapping table in the interop article is the starting point.
3. How to handle modifies clauses – these have no spec equivalent.

• Dafny-Clojure JVM Interop (parent article, SG-2 gap)
• Lean 4 codec proofs (the type-level version of this)
• Type systems, one tool four ways (comparative perspective)
• clojure.spec, since 2016 (spec.alpha vs malli as the output target)