diff --git a/SPEC.md b/SPEC.md
index e800a8d..26eff28 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -645,6 +645,8 @@ Lambda bodies can be expressions (`(x) => x + 1`) or statement blocks (`(x) => {
 
 Flat object destructuring in a lambda parameter is supported, including aliases (`({ id, hidden: isHidden }) => ...`). It remains one callback parameter and lowers to immutable field bindings inside the lambda. Array patterns, nested object patterns, defaults, and rest properties are rejected during extraction with an explicit unsupported-pattern error.
 
+Arrow lambdas used as expressions reject rest parameters during extraction: the lambda model does not collect callback arguments into a rest array.
+
 **filterMap.** `xs.map(x => ... | undefined).filter((x): x is T => x !== undefined)` drops the `undefined`s *and* unwraps to `seq<T>` — lowered to the proven `SeqFilterSome` preamble (a plain `Map(.value, Filter(.Some?, ...))` wouldn't verify, since `.value` is partial).
 
 **`.map` (Dafny).** Lowered to a `seq` comprehension with the element access inlined (`var x := arr[i]; e`), not `Seq.Map`. `Seq.Map` hides the element behind a closure, so a recursive rebuild walker (`Node(kids.map(walk))`) fails Dafny's termination check — the obligation gets quantified over the lambda's parameter instead of anchored at `kids[i]`. Applying a lambda inside the comprehension fails the same way, hence the inlining.
diff --git a/tools/src/extract.ts b/tools/src/extract.ts
index 795cd28..d0c1613 100644
--- a/tools/src/extract.ts
+++ b/tools/src/extract.ts
@@ -541,6 +541,9 @@ function extractExpr(node: Expression): RawExpr {
     // generated backend identifier.
     const destructureBindings: RawStmt[] = [];
     const params = node.getParameters().map((p, paramIndex) => {
+      if (p.isRestParameter()) {
+        throw new Error(`rest parameter in arrow lambda not yet supported: ${p.getText()}`);
+      }
       const typeNode = p.getTypeNode();
       const tsType = typeNode ? typeNode.getText() : undefined;
       const nameNode = p.getNameNode();
diff --git a/tools/tests/arrow-rest-parameters.test.ts b/tools/tests/arrow-rest-parameters.test.ts
new file mode 100644
index 0000000..e9192f3
--- /dev/null
+++ b/tools/tests/arrow-rest-parameters.test.ts
@@ -0,0 +1,56 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { Project, ScriptTarget } from "ts-morph";
+import { extractModule } from "../src/extract.ts";
+
+function extract(text: string) {
+  const project = new Project({ compilerOptions: { strict: true,
+    target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } });
+  const source = project.createSourceFile("rest.ts", text);
+  assert.deepEqual(project.getPreEmitDiagnostics(), [], "input must be valid TypeScript");
+  return extractModule(source);
+}
+
+test("map callbacks receive three arguments, rather than the array element's contents", () => {
+  const counts = [[7]].map((...args: (number | number[] | number[][])[]) => args.length);
+  assert.deepEqual(counts, [3]);
+  assert.deepEqual([[7]].map(value => value.length), [1]);
+});
+
+for (const [name, source] of [
+  ["map expression callback", `export function counts(): number[] {
+    return [[7]].map((...args: (number | number[] | number[][])[]) => args.length);
+  }`],
+  ["map block callback", `export function counts(): number[] {
+    return [[7]].map((...args: (number | number[] | number[][])[]) => { return args.length; });
+  }`],
+  ["some callback", `export function count(): boolean {
+    return [[7]].some((...args: (number | number[] | number[][])[]) => args.length === 1);
+  }`],
+  ["fixed parameter followed by rest", `export function counts(): number[] {
+    return [7].map((value, ...tail: (number | number[])[]) => tail.length);
+  }`],
+] as const) {
+  test(`extraction rejects rest parameters in a lambda: ${name}`, () => {
+    assert.throws(() => extract(source), /rest.*(lambda|arrow)|(lambda|arrow).*rest/i);
+  });
+}
+
+test("ordinary array parameters and object bindings remain supported", () => {
+  assert.doesNotThrow(() => extract(`
+    export function lengths(xs: number[][]): number[] { return xs.map(value => value.length); }
+    export function fields(xs: { value: number }[]): number[] { return xs.map(({value}) => value); }
+    export function many(xs: number[]): number[] { return xs.map((value, index) => value + index); }
+  `));
+});
+
+test("named variadic declarations retain their rest grouping metadata", () => {
+  const module = extract(`
+    export function named(...values: number[]): number { return values.length; }
+    export const arrow = (...values: number[]): number => values.length;
+  `);
+  assert.equal(module.functions.length, 2);
+  for (const fn of module.functions) {
+    assert.deepEqual(fn.tsParams, [{kind: "rest", binds: ["values"]}]);
+  }
+});