diff --git a/SPEC.md b/SPEC.md
index 84d8559..3834412 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -993,8 +993,11 @@ function tagNameExists(m: Model, name: string, excludeTag?: TagId): boolean {
 If `transformPureBody` can auto-convert the body to a pure expression, the function emits as a normal Dafny `function`. If it cannot (e.g., the body has loops), it emits as `function by method`:
 
 ```dafny
+function tagNameExists_fun_spec(m: Model, name: string, excludeTag: Option<TagId>): bool
+
 function tagNameExists(m: Model, name: string, excludeTag: Option<TagId>): bool
 {
+  tagNameExists_fun_spec(m, name, excludeTag)
 }
 by method {
   var i_tid_keys := SetToSeq(m.tags.Keys);
@@ -1002,21 +1005,18 @@ by method {
 }
 ```
 
-The empty `{ }` block is the spec body placeholder — **Dafny will reject the file as a parse error until it is filled in**. Complete it in the `.dfy` file *before* running verify:
+The functional body delegates to a bodyless `tagNameExists_fun_spec` stub, so the generated file parses and resolves on its own. Give the stub a body in the `.dfy` by adding lines after its signature:
 
 ```dafny
-function tagNameExists(m: Model, name: string, excludeTag: Option<TagId>): bool
+function tagNameExists_fun_spec(m: Model, name: string, excludeTag: Option<TagId>): bool
 {
   exists tid :: tid in m.tags &&
     (match excludeTag { case None => true case Some(v) => v != tid }) &&
     eqIgnoreCase(m.tags[tid].name, name)
 }
-by method {
-  // ... auto-generated, preserved by regen
-}
 ```
 
-The spec body is purely additive — `regen` three-way-merges and preserves user additions while updating the `by method` block when the TypeScript changes.
+Dafny then verifies that the `by method` block computes `tagNameExists_fun_spec`; left bodyless, the stub is uninterpreted and that proof fails. `regen` three-way-merges the `by method` block when the TypeScript changes without touching the added body.
 
 **Effect on callers:** Since `//@ pure` functions are `function`s in Dafny, callers that only invoke pure functions become pure automatically. For example, a large `switch`-based `apply` function becomes a `function` if all the map-iterating helpers it calls are marked `//@ pure`.
 
diff --git a/examples/countBadPairs.dfy b/examples/countBadPairs.dfy
index 2cee796..4ae5ca9 100644
--- a/examples/countBadPairs.dfy
+++ b/examples/countBadPairs.dfy
@@ -26,13 +26,19 @@ function JSFloorDiv(a: int, b: int): int
 datatype Pair = Pair(i: nat, j: nat)
 
 // ═════════════════════ Iterative impls (function by method) ═════════════════════
-// Spec body delegates to the matching hand-written predicate, so the
-// `by method` block verifies the imperative impl returns that set.
+// Each generated `<name>_spec` stub gets its body here: the matching
+// hand-written predicate, so the `by method` block verifies the imperative
+// impl returns that set.
 
-function allPairsImpl(nums: seq<int>): set<Pair>
+function allPairsImpl_fun_spec(nums: seq<int>): set<Pair>
 {
   AllPairs(nums)
 }
+
+function allPairsImpl(nums: seq<int>): set<Pair>
+{
+  allPairsImpl_fun_spec(nums)
+}
 by method {
   var result: set<Pair> := {};
   var i := 0;
@@ -60,10 +66,15 @@ by method {
   return result;
 }
 
-function goodPairsImpl(nums: seq<int>): set<Pair>
+function goodPairsImpl_fun_spec(nums: seq<int>): set<Pair>
 {
   GoodPairs(nums)
 }
+
+function goodPairsImpl(nums: seq<int>): set<Pair>
+{
+  goodPairsImpl_fun_spec(nums)
+}
 by method {
   var result: set<Pair> := {};
   var i := 0;
@@ -93,10 +104,15 @@ by method {
   return result;
 }
 
-function badPairsImpl(nums: seq<int>): set<Pair>
+function badPairsImpl_fun_spec(nums: seq<int>): set<Pair>
 {
   BadPairs(nums)
 }
+
+function badPairsImpl(nums: seq<int>): set<Pair>
+{
+  badPairsImpl_fun_spec(nums)
+}
 by method {
   var result: set<Pair> := {};
   var i := 0;
diff --git a/examples/countBadPairs.dfy.gen b/examples/countBadPairs.dfy.gen
index 92e5abd..1c66832 100644
--- a/examples/countBadPairs.dfy.gen
+++ b/examples/countBadPairs.dfy.gen
@@ -13,8 +13,11 @@ function JSFloorDiv(a: int, b: int): int
 
 datatype Pair = Pair(i: nat, j: nat)
 
+function allPairsImpl_fun_spec(nums: seq<int>): set<Pair>
+
 function allPairsImpl(nums: seq<int>): set<Pair>
 {
+  allPairsImpl_fun_spec(nums)
 }
 by method {
   var result: set<Pair> := {};
@@ -43,8 +46,11 @@ by method {
   return result;
 }
 
+function goodPairsImpl_fun_spec(nums: seq<int>): set<Pair>
+
 function goodPairsImpl(nums: seq<int>): set<Pair>
 {
+  goodPairsImpl_fun_spec(nums)
 }
 by method {
   var result: set<Pair> := {};
@@ -75,8 +81,11 @@ by method {
   return result;
 }
 
+function badPairsImpl_fun_spec(nums: seq<int>): set<Pair>
+
 function badPairsImpl(nums: seq<int>): set<Pair>
 {
+  badPairsImpl_fun_spec(nums)
 }
 by method {
   var result: set<Pair> := {};
diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts
index 6273ec5..58915a6 100644
--- a/tools/src/dafny-emit.ts
+++ b/tools/src/dafny-emit.ts
@@ -11,6 +11,8 @@ import { DEFAULT_OPTIONS, resolveOptions, type LscOptions } from "./config.js";
 
 /** Appended to a function's name for the lemma that carries its `//@ ensures`. */
 export const ENSURES_LEMMA_SUFFIX = "_ensures";
+/** `function by method` bodies delegate to a proof-defined `<name>_fun_spec`. */
+export const SPEC_FUNCTION_SUFFIX = "_fun_spec";
 
 /** Fresh binder for a comprehension wrapping the given subexpressions: `base`
  *  verbatim unless one of them references it, then primed until free. A *local*
@@ -973,10 +975,21 @@ function emitDecl(d: Decl): string {
 
     case "def-by-method": {
       const tp = d.typeParams.length > 0 ? `<${d.typeParams.join(", ")}>` : "";
-      const lines = [`function ${escapeName(d.name)}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`];
-      for (const r of d.requires) lines.push(`  requires ${emitExpr(r)}`);
+      const signature = `${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`;
+      const requires = d.requires.map(r => `  requires ${emitExpr(r)}`);
+      // The functional specification is the proof author's to write: a bodyless
+      // `<name>_fun_spec` stub, which the .dfy completes by adding a body after its
+      // signature. The generated file parses and resolves on its own (an empty
+      // function body would not), and the proof adds lines instead of editing
+      // between generated braces.
+      const spec = escapeGeneratedName(`${d.name}${SPEC_FUNCTION_SUFFIX}`);
+      const lines = [
+        `function ${spec}${signature}`, ...requires, "",
+        `function ${escapeName(d.name)}${signature}`, ...requires,
+      ];
       if (d.decreases) lines.push(`  decreases ${emitExpr(d.decreases)}`);
       lines.push(`{`);
+      lines.push(`  ${spec}(${d.params.map(p => escapeName(p.name)).join(", ")})`);
       lines.push(`}`);
       lines.push(`by method {`);
       lines.push(emitStmts(d.methodBody, 1));