diff --git a/packages/amico-run/src/schemas.ts b/packages/amico-run/src/schemas.ts
index 1f0958f4..60cd7d81 100644
--- a/packages/amico-run/src/schemas.ts
+++ b/packages/amico-run/src/schemas.ts
@@ -17,6 +17,10 @@ export function validateFinished(v: unknown): Validation {
   return validate(v, "finished");
 }
 
+export function validateFormulation(v: unknown): Validation {
+  return validate(v, "formulation");
+}
+
 export function validateResult(v: unknown): Validation {
   return validate(v, "result");
 }
diff --git a/packages/amico-run/test/schemas.test.ts b/packages/amico-run/test/schemas.test.ts
index 04296653..4e2f7ac4 100644
--- a/packages/amico-run/test/schemas.test.ts
+++ b/packages/amico-run/test/schemas.test.ts
@@ -1,7 +1,7 @@
 import { describe, it, expect } from 'vitest'
 import { readFileSync } from 'node:fs'
 import { join } from 'node:path'
-import { validateManifest, validateFinished, validateResult } from '../src/schemas.js'
+import { validateManifest, validateFinished, validateResult, validateFormulation } from '../src/schemas.js'
 
 // These wrappers delegate to the shared @amicode/schema (single source of truth);
 // this suite is the delegation smoke + the field-precise contract they expose.
@@ -43,6 +43,21 @@ describe('validateResult (reader-side)', () => {
   })
 })
 
+describe('validateFormulation (reader-side)', () => {
+  it('requires schema_version + system.family + formulation.gate; leaves lenient per family', () => {
+    // The pre-solve problem-definition file (#64 counterpart). Structure fixed,
+    // leaf params lenient per family (a rydberg [system] carries no delta).
+    expect(validateFormulation({
+      schema_version: '1',
+      system: { family: 'transmon', delta: 0.2, levels: 3, drive_max: 0.2 },
+      formulation: { gate: 'X', T: 10.0, N: 50, Q: 100.0, R: 0.01 },
+    }).ok).toBe(true)
+    expect(validateFormulation({ system: { family: 'transmon' }, formulation: { gate: 'X' } }).ok).toBe(false) // no schema_version
+    expect(validateFormulation({ schema_version: '1', system: {}, formulation: { gate: 'X' } }).ok).toBe(false) // no family
+    expect(validateFormulation({ schema_version: '1', system: { family: 'transmon' }, formulation: {} }).ok).toBe(false) // no gate
+  })
+})
+
 // Anti-regression (N4): schemas.ts must remain a thin DELEGATION, never re-define
 // a schema/validator. Guards the "one validator path" invariant (#15 AC7).
 describe('schemas.ts is delegation-only (no re-introduced schema)', () => {
diff --git a/packages/extension/src/file_watcher.ts b/packages/extension/src/file_watcher.ts
index 5a960491..d8f09cc0 100644
--- a/packages/extension/src/file_watcher.ts
+++ b/packages/extension/src/file_watcher.ts
@@ -6,7 +6,7 @@ import { getInspector } from "./run_inspector";
 import type { StatusBarManager } from "./status_bar";
 import type { RunStatus } from "./types";
 import {
-  AMICODE_ITER_RE, ingestRunDir, readTomlSafe, parseAmicoNum, PulseStream, SinkDedup,
+  AMICODE_ITER_RE, ingestRunDir, readTomlSafe, readFormulation, parseAmicoNum, PulseStream, SinkDedup,
   type IterRecord, type PulseEvent, type RunCompletion, type PromoteInfo, type RunSink,
 } from "./run_dir_reader";
 
@@ -247,7 +247,10 @@ export class RunsRootWatcher implements vscode.Disposable {
         else this.opts.channel.appendLine(`[runs] result.toml present but invalid: ${v.errors.join("; ")}`);
       }
     }
-    this.sink?.run({ runId, runDir, status, fidelity });
+    // Same read as the replay path (shared helper — the two completion routes
+    // can't diverge on whether a live-finished run carries its formulation).
+    const formulation = readFormulation(runDir);
+    this.sink?.run({ runId, runDir, status, fidelity, formulation });
     if (status === "completed" && fidelity !== undefined && fidelity >= (this.opts.promoteThreshold ?? 0.99)) {
       this.sink?.promote({ runId, runDir, fidelity });
     }
diff --git a/packages/extension/src/run_dir_reader.ts b/packages/extension/src/run_dir_reader.ts
index c07f5acc..52ea0754 100644
--- a/packages/extension/src/run_dir_reader.ts
+++ b/packages/extension/src/run_dir_reader.ts
@@ -1,7 +1,7 @@
 import * as fs from "node:fs";
 import * as path from "node:path";
 import { parse } from "smol-toml";
-import { validateManifest, validateFinished, validateResult } from "@amicode/amico-run";
+import { validateManifest, validateFinished, validateResult, validateFormulation } from "@amicode/amico-run";
 import type { RunStatus } from "./types";
 
 // ============================================================================
@@ -105,7 +105,13 @@ export class PulseStream {
 }
 
 export interface IterRecord { iter: number; f_val: number; inf_pr: number; inf_du: number }
-export interface RunCompletion { runId: string; runDir: string; status: RunStatus; fidelity?: number }
+
+/** The pre-solve problem definition, surfaced from formulation.toml when present
+ *  and valid (additive to the run-dir contract). `[system]`/`[formulation]` are
+ *  lenient leaf-field bags per family (see formulation.schema.json), so this is
+ *  intentionally loose; the only guaranteed keys are system.family + formulation.gate. */
+export interface Formulation { system: Record<string, unknown>; formulation: Record<string, unknown> }
+export interface RunCompletion { runId: string; runDir: string; status: RunStatus; fidelity?: number; formulation?: Formulation }
 export interface PromoteInfo { runId: string; runDir: string; fidelity: number }
 
 /** Where ingestRunDir routes its findings. The live impl carries the
@@ -136,6 +142,18 @@ export function readTomlSafe(fp: string): Record<string, unknown> | undefined {
   catch { return undefined; }
 }
 
+/** Read + validate formulation.toml (#64 counterpart) — additive, absent → undefined.
+ *  Shared by BOTH completion routes (ingestRunDir replay + the live-finish path) so
+ *  they can't diverge on whether a run carries its problem identity. Say-why-on-
+ *  invalid; never throws. */
+export function readFormulation(runDir: string): Formulation | undefined {
+  const raw = readTomlSafe(path.join(runDir, "formulation.toml"));
+  if (!raw) return undefined;
+  const v = validateFormulation(raw);
+  if (!v.ok) { console.warn(`[amico] formulation.toml present but invalid (${runDir}): ${v.errors.join("; ")}`); return undefined; }
+  return { system: raw.system as Record<string, unknown>, formulation: raw.formulation as Record<string, unknown> };
+}
+
 /** Pure, stateless replay of a run dir against the β.1 contract. Calls each
  *  sink method at most once per relevant artifact. Safe to re-invoke (the live
  *  sink's guards make it idempotent). Returns the number of run.log bytes
@@ -169,6 +187,11 @@ export function ingestRunDir(runDir: string, sink: RunSink, promoteThreshold = 0
     if (newestPulse) sink.pulse(newestPulse);
   }
 
+  // formulation.toml (#64 counterpart) — the pre-solve problem definition, read via
+  // the shared readFormulation helper so this replay path and the live-finish path
+  // stay in lockstep (additive; absent → undefined, older runs unchanged).
+  const formulation = readFormulation(runDir);
+
   // FINISHED is the authoritative terminal signal
   const finished = readTomlSafe(path.join(runDir, "FINISHED"));
   if (!finished || !validateFinished(finished).ok) return logBytes;
@@ -186,7 +209,7 @@ export function ingestRunDir(runDir: string, sink: RunSink, promoteThreshold = 0
       else console.warn(`[amico] result.toml present but invalid (${runDir}): ${v.errors.join("; ")}`);
     }
   }
-  sink.run({ runId, runDir, status, fidelity });
+  sink.run({ runId, runDir, status, fidelity, formulation });
   if (status === "completed" && fidelity !== undefined && fidelity >= promoteThreshold) {
     sink.promote({ runId, runDir, fidelity });
   }
diff --git a/packages/extension/templates/solve_template.jl b/packages/extension/templates/solve_template.jl
index c971dac2..ef58cfb0 100644
--- a/packages/extension/templates/solve_template.jl
+++ b/packages/extension/templates/solve_template.jl
@@ -11,13 +11,20 @@ using TOML
 using Printf
 
 # ── FILL IN ──────────────────────────────────────────────────────────────
-δ          = 0.2        # anharmonicity (GHz, positive convention)
-levels     = 3          # transmon levels modeled (3 = qubit + 1 leakage; bump to 4–5 for more leakage realism)
-gate       = GATES[:X]
-T          = 10.0       # gate time (ns)
-N          = 50         # timesteps
-drive_max  = 0.2        # per-quadrature drive bound (GHz)
-max_iter   = 60
+δ           = 0.2        # anharmonicity (GHz, positive convention)
+levels      = 3          # transmon levels modeled (3 = qubit + 1 leakage; bump to 4–5 for more leakage realism)
+# Standard gate — the symbol is the single source: it drives both the matrix AND the
+# label, so they can't drift (GATES[:X] is a matrix; the ":X" name is otherwise lost).
+gate_sym    = :X
+gate        = GATES[gate_sym]
+gate_name   = string(gate_sym)
+# — Bespoke gate NOT in the (deliberately sparse) GATES set (cat / Fock-mix / CXX / ZZ…)?
+#   Declare both directly — there's no symbol to derive from:  gate = my_unitary; gate_name = "cat-CZ"
+system_name = nothing    # optional user-assigned device name (e.g. "qram-cleland"); nothing if unnamed
+T           = 10.0       # gate time (ns)
+N           = 50         # timesteps
+drive_max   = 0.2        # per-quadrature drive bound (GHz)
+max_iter    = 60
 # ─────────────────────────────────────────────────────────────────────────
 
 sys = TransmonSystem(; δ = δ, levels = levels, drive_bounds = fill(drive_max, 2))
@@ -26,11 +33,63 @@ op  = size(gate, 1) == sys.levels ? gate : EmbeddedOperator(gate, sys)
 times   = collect(range(0.0, T, length = N))
 initial = 0.1 * randn(sys.n_drives, N)
 qtraj = UnitaryTrajectory(sys, ZeroOrderPulse(initial, times), op)
+Q = 100.0   # infidelity objective weight — defines the optimum (recorded in formulation.toml)
+R = 1e-2    # control-effort objective weight — defines the optimum (recorded in formulation.toml)
 qcp = SmoothPulseProblem(qtraj, N;
     piccolo_options = PiccoloOptions(timesteps_all_equal = true),
-    Q = 100.0, R = 1e-2)
+    Q = Q, R = R)
 prob = hasproperty(qcp, :prob) ? qcp.prob : qcp
 
+# Pre-solve run-dir emit helper: writes formulation.toml (the DECLARED problem —
+# physics + objective), the authoritative identity source #64 keys hashes off.
+# Defined INLINE — NOT include(joinpath(@__DIR__, "...")): AGENTS.md deploys this
+# template by copying THIS FILE ALONE into a scratch dir and running the copy, so
+# @__DIR__ is that scratch dir and a sibling include resolves to a file that was
+# never copied (LoadError before solve!). When a second template needs this, lift
+# it verbatim into a Julia package (AmicoRunDir.jl) resolved via `using` — the only
+# share mechanism that survives the single-file copy.
+#
+# Contract (validated by @amicode/schema formulation.schema.json):
+#   [system]      family (required) + optional name + family-dependent params
+#   [formulation] gate + T + N (required) + optional Q/R + family-dependent extras
+# system_params / formulation_extra are merged per family (the schema constrains
+# known families but tolerates unknown leaves), so a rydberg caller can pass
+# Omega_max/C6/... with no edit here.
+function emit_formulation(;
+    system_family::AbstractString,
+    gate_name::AbstractString,
+    system_params::AbstractDict = Dict{String,Any}(),
+    system_name::Union{AbstractString,Nothing} = nothing,
+    formulation_extra::AbstractDict = Dict{String,Any}(),
+    path::AbstractString = "formulation.toml",
+)
+    system = Dict{String,Any}("family" => String(system_family))
+    if system_name !== nothing
+        system["name"] = String(system_name)
+    end
+    for (k, v) in system_params
+        system[String(k)] = v
+    end
+
+    formulation = Dict{String,Any}("gate" => String(gate_name))
+    for (k, v) in formulation_extra
+        formulation[String(k)] = v
+    end
+
+    doc = Dict{String,Any}(
+        "schema_version" => "1",   # run-dir contract version (@amicode/schema formulation schema)
+        "system" => system,
+        "formulation" => formulation,
+    )
+
+    tmp = path * ".tmp"
+    open(tmp, "w") do io
+        TOML.print(io, doc)
+    end
+    mv(tmp, path; force = true)   # atomic swap — a partial read never sees a half-written file
+    return path
+end
+
 # Per-iter live plot flows through Piccolo's `LivePulsePlotCallback`, an
 # `AbstractIntermediateCallback` (the blessed, solver-agnostic per-iter plot
 # idiom — see AGENTS.md). It reconstructs the pulse from the optimizer's primal
@@ -86,6 +145,18 @@ let ls = join(("\"a_$i\"" for i in 1:sys.n_drives), ","),
     flush(stdout)
 end
 
+# Pre-solve: drop formulation.toml — the DECLARED problem (physics + objective),
+# written before solve! while every FILL-IN var is in scope. Authoritative
+# identity source (#64 keys hashes off this); [system] = the device, [formulation]
+# = the optimal-control problem posed against it.
+emit_formulation(;
+    system_family = "transmon",
+    gate_name = gate_name,
+    system_name = system_name,
+    system_params = Dict("delta" => δ, "levels" => levels, "drive_max" => drive_max),
+    formulation_extra = Dict("T" => T, "N" => N, "Q" => Q, "R" => R),
+)
+
 # AMICODE_ITER text telemetry stays on the RAW Ipopt callback — it needs the rich
 # IPM state (obj_value/inf_pr/inf_du) that the agnostic `(primal, iter)` contract
 # doesn't carry. Both callbacks fire once per iteration (DTO composes the raw
@@ -132,6 +203,10 @@ JLD2.save("pulse.jld2", "traj", prob.trajectory)   # key "traj" so `load_traj` c
 open("result.toml.tmp", "w") do io
     # Record the regime each run actually solved (scalar FILL-IN params), so the
     # result is self-describing — not just fidelity/iterations.
+    # NOTE: [params] is now REDUNDANT with the pre-solve formulation.toml (the
+    # authoritative problem-definition file). Kept for now so in-flight consumers
+    # (#73 card reads params.T/params.system) don't break; killing it is a
+    # follow-up once those readers migrate to formulation.toml (tracked in #64).
     TOML.print(io, Dict(
         "schema_version" => "1",   # run-dir contract version (@amicode/schema result schema)
         "fidelity" => fid, "iterations" => iters[], "wall_seconds" => wall,
diff --git a/packages/extension/test/template_deploy_contract.test.ts b/packages/extension/test/template_deploy_contract.test.ts
new file mode 100644
index 00000000..ab6b79a4
--- /dev/null
+++ b/packages/extension/test/template_deploy_contract.test.ts
@@ -0,0 +1,57 @@
+import { describe, it, expect } from 'vitest'
+import { mkdtempSync, copyFileSync, existsSync, readFileSync } from 'node:fs'
+import { tmpdir } from 'node:os'
+import { basename, join } from 'node:path'
+
+// Regression guard (#81). DEPLOYMENT REALITY: AGENTS.md tells the agent to COPY the
+// solve template into a scratch dir and run THAT copy — `julia <scratch>/solve.jl`
+// (see AGENTS.md "Workflow" step 2/3). So inside the running script @__DIR__ is the
+// scratch dir, NOT the bundled templates dir — and any sibling `include(@__DIR__/…)`
+// opens a file only present if the deploy step also copied it. #81's first draft added
+// `include(joinpath(@__DIR__, "emit_formulation.jl"))` while AGENTS.md copies only the
+// template → LoadError before solve!, on every agent-driven run. Nothing in the vitest
+// suite executed the template, so it shipped green. This test closes that gap WITHOUT
+// needing Julia: it ties the two seams together — reproduce exactly the files AGENTS.md
+// copies into scratch, then assert every include() in the deployed script resolves there.
+// Stays green under either fix: inline the helper (no include), or teach AGENTS.md to
+// copy it too. The deeper guard is #78's smoke corpus actually running a solve.
+const EXT = join(__dirname, '..')
+const AGENTS = readFileSync(join(EXT, 'AGENTS.md'), 'utf8')
+const TEMPLATE = join(EXT, 'templates', 'solve_template.jl')
+
+describe('solve template deploys runnably under AGENTS.md single-file copy [#81]', () => {
+  it('every include() in the deployed script resolves in the scratch dir', () => {
+    const scratch = mkdtempSync(join(tmpdir(), 'amicode-work-'))
+
+    // Reproduce AGENTS.md's scratch-dir copies: `cp <src> /tmp/amicode-work/<dst>`.
+    // {{TEMPLATE_PATH}} is the substitution for the bundled solve_template.jl.
+    const copied = new Map<string, string>()   // destName -> srcAbs
+    for (const m of AGENTS.matchAll(/\bcp\s+(\S+)\s+(\S+)/g)) {
+      const [, srcTok, dst] = m
+      if (!dst.includes('amicode-work')) continue
+      const srcAbs = srcTok.replace('{{TEMPLATE_PATH}}', TEMPLATE)
+      copied.set(dst.endsWith('/') ? basename(srcAbs) : basename(dst), srcAbs)
+    }
+    expect(copied.size, 'AGENTS.md should document copying the template into the scratch dir').toBeGreaterThan(0)
+    for (const [name, srcAbs] of copied) copyFileSync(srcAbs, join(scratch, name))
+
+    // amico-run runs `julia <scratch>/solve.jl`, so @__DIR__ === scratch for the run file.
+    const runFile = copied.has('solve.jl') ? 'solve.jl' : [...copied.keys()][0]
+    const src = readFileSync(join(scratch, runFile), 'utf8')
+
+    // Julia resolves a relative include (bare or joinpath(@__DIR__, …)) against @__DIR__.
+    const unresolved: string[] = []
+    for (const m of src.matchAll(/^[ \t]*include\((.+?)\)[ \t]*(?:#.*)?$/gm)) {
+      const arg = m[1].trim()
+      const sibling =
+        arg.match(/^joinpath\(\s*@__DIR__\s*,\s*"([^"]+)"\s*\)$/)?.[1] ??
+        arg.match(/^"(?!\/)([^"]+)"$/)?.[1]
+      if (sibling === undefined) { unresolved.push(`unclassifiable include(${arg})`); continue }
+      if (!existsSync(join(scratch, sibling))) unresolved.push(sibling)
+    }
+    expect(
+      unresolved,
+      `deployed template can't resolve include(s): ${unresolved.join(', ')} — inline them, or make AGENTS.md copy them into the scratch dir`,
+    ).toEqual([])
+  })
+})
diff --git a/packages/extension/test/watcher_contract.test.ts b/packages/extension/test/watcher_contract.test.ts
index ff86d049..9d618e5b 100644
--- a/packages/extension/test/watcher_contract.test.ts
+++ b/packages/extension/test/watcher_contract.test.ts
@@ -4,7 +4,13 @@ import { tmpdir } from 'node:os'
 import { join } from 'node:path'
 import { ingestRunDir, AMICODE_ITER_RE, parseAmicoNum, parsePulseMetaLine, parsePulseRecordLine, PulseStream, SinkDedup } from '../src/run_dir_reader'   // pure β.1-contract reader (vscode-free)
 
-function stageRun(opts: { status: string; exit: number; iters: number[]; fidelity?: number }): string {
+const VALID_FORMULATION =
+  'schema_version = "1"\n[system]\nfamily = "transmon"\nname = "qram-cleland"\nlevels = 3\ndelta = 0.2\ndrive_max = 0.2\n' +
+  '[formulation]\ngate = "X"\nT = 10.0\nN = 50\nQ = 100.0\nR = 0.01\n'
+// nonconforming: [system] has no family, [formulation] has no gate (the two DECLARED-label requireds)
+const INVALID_FORMULATION = 'schema_version = "1"\n[system]\nlevels = 3\n[formulation]\nT = 10.0\n'
+
+function stageRun(opts: { status: string; exit: number; iters: number[]; fidelity?: number; formulation?: string }): string {
   const root = mkdtempSync(join(tmpdir(), 'runs-'))
   const runId = 'r20260615-000000Z-ab12'
   const dir = join(root, runId); mkdirSync(dir, { recursive: true })
@@ -12,6 +18,7 @@ function stageRun(opts: { status: string; exit: number; iters: number[]; fidelit
     `schema_version = "1"\nrun_id = "${runId}"\nscript_path = "/s.jl"\nlab = "default"\nlab_id = "default"\ncreated_at = "2026-06-15T00:00:00Z"\norchestrator_version = "0.1.0"\n[julia]\nbinary = "julia"\n`)
   writeFileSync(join(dir, 'run.log'), opts.iters.map(k => `AMICODE_ITER iter=${k} f=0.1 inf_pr=1e-8 inf_du=1e-6`).join('\n') + '\n')
   if (opts.fidelity !== undefined) writeFileSync(join(dir, 'result.toml'), `schema_version = "1"\nfidelity = ${opts.fidelity}\niterations = ${Math.max(...opts.iters, 0)}\n`)
+  if (opts.formulation !== undefined) writeFileSync(join(dir, 'formulation.toml'), opts.formulation)
   writeFileSync(join(dir, 'FINISHED'), `status = "${opts.status}"\nexit_code = ${opts.exit}\n`)
   return dir
 }
@@ -71,6 +78,42 @@ describe('ingestRunDir — β.1 contract reading (replay)', () => {
   })
 })
 
+// formulation.toml (#64 counterpart) — the pre-solve problem-definition file.
+// Additive to the reader: present+valid → surfaced on the completion record;
+// absent → undefined (older runs unchanged); present+invalid → dropped, run still reported.
+describe('ingestRunDir — formulation.toml surfacing (additive)', () => {
+  it('present + valid: surfaces [system]/[formulation] on the completion record', () => {
+    const sink = fakeSink()
+    ingestRunDir(stageRun({ status: 'completed', exit: 0, iters: [1], fidelity: 0.999, formulation: VALID_FORMULATION }), sink)
+    expect(sink.run).toHaveBeenCalledWith(expect.objectContaining({
+      status: 'completed',
+      formulation: {
+        system: expect.objectContaining({ family: 'transmon', name: 'qram-cleland', delta: 0.2 }),
+        formulation: expect.objectContaining({ gate: 'X', T: 10.0, N: 50, Q: 100.0, R: 0.01 }),
+      },
+    }))
+  })
+
+  it('absent: completion record carries no formulation (older runs unchanged)', () => {
+    const sink = fakeSink()
+    ingestRunDir(stageRun({ status: 'completed', exit: 0, iters: [1], fidelity: 0.999 }), sink)
+    expect(sink.run).toHaveBeenCalledTimes(1)
+    expect(sink.run.mock.calls[0][0].formulation).toBeUndefined()
+    expect(sink.run).toHaveBeenCalledWith(expect.objectContaining({ status: 'completed', fidelity: 0.999 }))
+  })
+
+  it('present but invalid: dropped (formulation undefined), run still reported + still promotes', () => {
+    const warn = vi.spyOn(console, 'warn').mockImplementation(() => {})
+    const sink = fakeSink()
+    ingestRunDir(stageRun({ status: 'completed', exit: 0, iters: [1], fidelity: 0.999, formulation: INVALID_FORMULATION }), sink)
+    expect(sink.run.mock.calls[0][0].formulation).toBeUndefined()   // invalid → not surfaced
+    expect(sink.run).toHaveBeenCalledWith(expect.objectContaining({ status: 'completed', fidelity: 0.999 }))
+    expect(sink.promote).toHaveBeenCalled()                          // fidelity path untouched
+    expect(warn).toHaveBeenCalledWith(expect.stringContaining('formulation.toml present but invalid'))
+    warn.mockRestore()
+  })
+})
+
 describe('AMICODE_ITER parsing — Inf/NaN are kept, not dropped', () => {
   it('matches blow-up / stagnation iters (Inf, -Inf, NaN), matching amico-run', () => {
     expect(AMICODE_ITER_RE.test('AMICODE_ITER iter=3 f=Inf inf_pr=NaN inf_du=-Inf')).toBe(true)
diff --git a/packages/schema/package.json b/packages/schema/package.json
index 0d1604a6..25300aae 100644
--- a/packages/schema/package.json
+++ b/packages/schema/package.json
@@ -1,6 +1,6 @@
 {
   "name": "@amicode/schema",
-  "version": "0.1.0",
+  "version": "0.2.0",
   "license": "Apache-2.0",
   "type": "module",
   "main": "./src/index.ts",
diff --git a/packages/schema/schemas/formulation.schema.json b/packages/schema/schemas/formulation.schema.json
new file mode 100644
index 00000000..1e6163d7
--- /dev/null
+++ b/packages/schema/schemas/formulation.schema.json
@@ -0,0 +1,48 @@
+{
+  "$schema": "http://json-schema.org/draft-07/schema#",
+  "$id": "https://amico.harmoniqs.co/schema/formulation/v1",
+  "title": "amico run-dir formulation.toml",
+  "description": "The PROBLEM a run was asked to solve — the physics and objective, written PRE-SOLVE by the Julia template. Split into [system] (the physical device) and [formulation] (the optimal-control problem posed against it). Additive third file in the run-dir contract (alongside run.toml / result.toml); it is the authoritative identity source #64's hashing keys off. The STRUCTURE is fixed (schema_version + [system] + [formulation]). Leaf fields are constrained PER FAMILY via conditional (if/then) branches keyed on system.family: a KNOWN family requires + type-checks its identity params (transmon: delta/levels/drive_max), while an UNKNOWN family stays lenient (additionalProperties: true) so a new device type validates before its branch lands. Add a family's constraints in the same change as that family's producer template — that keeps every such tightening additive (no pre-existing on-disk data of that family to break), so it never forces a schema_version bump.",
+  "type": "object",
+  "additionalProperties": false,
+  "required": ["schema_version", "system", "formulation"],
+  "properties": {
+    "schema_version": { "enum": ["1"], "description": "run-dir contract version (enum = the supported-version SET; grows by one entry per bump)" },
+    "system": {
+      "type": "object",
+      "description": "The physical device being driven — independent of the gate asked of it. Only the family label is required at this level; each KNOWN family adds its own required + typed leaves via the allOf/if-then branches below (transmon: delta/levels/drive_max). additionalProperties stays true so a family can carry extra params, and an unknown family validates leniently until its branch is added.",
+      "additionalProperties": true,
+      "required": ["family"],
+      "properties": {
+        "family": { "type": "string", "minLength": 1, "description": "DECLARED family label (the family/type of system, e.g. \"transmon\", \"rydberg\") — cannot be reverse-derived from the Julia struct's type, so the template declares it" },
+        "name": { "type": "string", "description": "optional user-assigned device name (from the #73 save flow, if named)" }
+      },
+      "allOf": [
+        {
+          "if": { "properties": { "family": { "const": "transmon" } }, "required": ["family"] },
+          "then": {
+            "required": ["delta", "levels", "drive_max"],
+            "properties": {
+              "delta": { "type": "number", "description": "anharmonicity δ (GHz, positive convention)" },
+              "levels": { "type": "integer", "minimum": 2, "description": "transmon levels modeled (2 = ideal qubit; 3 = qubit + 1 leakage)" },
+              "drive_max": { "type": "number", "exclusiveMinimum": 0, "description": "per-quadrature drive bound (GHz)" }
+            }
+          }
+        }
+      ]
+    },
+    "formulation": {
+      "type": "object",
+      "description": "The optimal-control problem posed against [system]: the target gate, time horizon, and objective weights. gate + T + N are the family-independent core every formulation carries; Q/R are optional (a family may weight its objective differently or not at all). additionalProperties stays true for family-dependent extras.",
+      "additionalProperties": true,
+      "required": ["gate", "T", "N"],
+      "properties": {
+        "gate": { "type": "string", "minLength": 1, "description": "DECLARED gate label (e.g. \"X\", \"CZ\") — GATES[:X] is a matrix, so the name is lost on that line; the template declares it" },
+        "T": { "type": "number", "exclusiveMinimum": 0, "description": "gate-time horizon (ns)" },
+        "N": { "type": "integer", "minimum": 1, "description": "timesteps" },
+        "Q": { "type": "number", "description": "infidelity objective weight (optional — defines the optimum when present)" },
+        "R": { "type": "number", "description": "control-effort objective weight (optional — defines the optimum when present)" }
+      }
+    }
+  }
+}
diff --git a/packages/schema/src/index.ts b/packages/schema/src/index.ts
index 8fc5e8be..7e05e7d4 100644
--- a/packages/schema/src/index.ts
+++ b/packages/schema/src/index.ts
@@ -11,6 +11,7 @@ import addFormatsDefault from "ajv-formats";
 
 import runSchema from "../schemas/run.schema.json" with { type: "json" };
 import finishedSchema from "../schemas/finished.schema.json" with { type: "json" };
+import formulationSchema from "../schemas/formulation.schema.json" with { type: "json" };
 import resultSchema from "../schemas/result.schema.json" with { type: "json" };
 import labSchema from "../schemas/lab.schema.json" with { type: "json" };
 import solvespecSchema from "../schemas/solvespec.schema.json" with { type: "json" };
@@ -27,6 +28,7 @@ const addFormats = (typeof addFormatsDefault === "function"
 const SCHEMAS = {
   run: runSchema,
   finished: finishedSchema,
+  formulation: formulationSchema,
   result: resultSchema,
   lab: labSchema,
   solvespec: solvespecSchema,
@@ -49,6 +51,7 @@ export interface Validation { ok: boolean; errors: string[] }
 export function kindForFilename(filePath: string): SchemaKind | undefined {
   const base = filePath.replace(/^.*[\\/]/, "");
   if (base === "run.toml") return "run";
+  if (base === "formulation.toml") return "formulation";
   if (base === "result.toml") return "result";
   if (base === "lab.toml") return "lab";
   if (base === "FINISHED") return "finished";
diff --git a/packages/schema/test/fixtures/invalid/formulation.toml b/packages/schema/test/fixtures/invalid/formulation.toml
new file mode 100644
index 00000000..8c09499c
--- /dev/null
+++ b/packages/schema/test/fixtures/invalid/formulation.toml
@@ -0,0 +1,9 @@
+schema_version = "1"
+
+[system]
+name = "qram-cleland"
+levels = 3
+
+[formulation]
+T = 10.0
+N = 50
diff --git a/packages/schema/test/fixtures/valid/formulation.toml b/packages/schema/test/fixtures/valid/formulation.toml
new file mode 100644
index 00000000..2a23ef93
--- /dev/null
+++ b/packages/schema/test/fixtures/valid/formulation.toml
@@ -0,0 +1,15 @@
+schema_version = "1"
+
+[system]
+family = "transmon"
+name = "qram-cleland"
+levels = 3
+delta = 0.2
+drive_max = 0.2
+
+[formulation]
+gate = "X"
+T = 10.0
+N = 50
+Q = 100.0
+R = 0.01
diff --git a/packages/schema/test/validate.test.ts b/packages/schema/test/validate.test.ts
index 661787a0..e2c071a8 100644
--- a/packages/schema/test/validate.test.ts
+++ b/packages/schema/test/validate.test.ts
@@ -26,9 +26,9 @@ describe("valid golden fixtures validate clean", () => {
 });
 
 describe("schema set + exports", () => {
-  it("exposes all five versioned schemas + the FINISHED sub-shape", () => {
+  it("exposes all versioned schemas + the FINISHED sub-shape", () => {
     expect(new Set(SCHEMA_KINDS)).toEqual(
-      new Set(["run", "result", "lab", "solvespec", "catalog-entry", "finished"]),
+      new Set(["run", "result", "formulation", "lab", "solvespec", "catalog-entry", "finished"]),
     );
   });
   it("SUPPORTED_SCHEMA_VERSIONS is the v1 instantiation of a version SET", () => {
@@ -43,16 +43,16 @@ describe("schema set + exports", () => {
 
 // ── schema_version policy (S5/S6, #15 AC3, #16 AC5, #17 AC3) ──
 describe("schema_version policy", () => {
-  it("ABSENT version → field-precise missing-required (the five versioned schemas)", () => {
-    for (const kind of ["run", "result", "lab", "solvespec", "catalog-entry"] as SchemaKind[]) {
+  it("ABSENT version → field-precise missing-required (the versioned schemas)", () => {
+    for (const kind of ["run", "result", "formulation", "lab", "solvespec", "catalog-entry"] as SchemaKind[]) {
       const obj = load(kind); delete obj.schema_version;
       const r = validate(obj, kind);
       expect(r.ok).toBe(false);
       expect(hasErr(r.errors, "missing required key \"schema_version\"")).toBe(true);
     }
   });
-  it("UNRECOGNIZED version → distinct version-specific error (all five versioned schemas)", () => {
-    for (const kind of ["run", "result", "lab", "solvespec", "catalog-entry"] as SchemaKind[]) {
+  it("UNRECOGNIZED version → distinct version-specific error (all versioned schemas)", () => {
+    for (const kind of ["run", "result", "formulation", "lab", "solvespec", "catalog-entry"] as SchemaKind[]) {
       const obj = load(kind); obj.schema_version = "99";
       const r = validate(obj, kind);
       expect(r.ok).toBe(false);
@@ -61,7 +61,7 @@ describe("schema_version policy", () => {
   });
   it("every versioned schema's enum is in sync with SUPPORTED_SCHEMA_VERSIONS (no drift seam)", () => {
     const schemasDir = join(here, "..", "schemas");
-    for (const kind of ["run", "result", "lab", "solvespec", "catalog-entry"]) {
+    for (const kind of ["run", "result", "formulation", "lab", "solvespec", "catalog-entry"]) {
       const schema = JSON.parse(readFileSync(join(schemasDir, `${kind}.schema.json`), "utf8"));
       expect(schema.properties.schema_version.enum, `${kind} enum drift`).toEqual([...SUPPORTED_SCHEMA_VERSIONS]);
     }
@@ -131,6 +131,67 @@ describe("field-precise negative matrix", () => {
   });
 });
 
+// ── formulation.toml — the pre-solve problem-definition file (#64 counterpart) ──
+describe("formulation.toml schema (System÷Formulation)", () => {
+  it("the valid fixture (transmon) validates clean", () => {
+    expect(validateFile(fixtureFile("formulation"), "formulation").errors).toEqual([]);
+  });
+  it("requires system.family and formulation.gate (the DECLARED labels)", () => {
+    const noFamily = load("formulation");
+    delete (noFamily.system as Record<string, unknown>).family;
+    expect(hasErr(validate(noFamily, "formulation").errors, '/system: missing required key "family"')).toBe(true);
+    const noGate = load("formulation");
+    delete (noGate.formulation as Record<string, unknown>).gate;
+    expect(hasErr(validate(noGate, "formulation").errors, '/formulation: missing required key "gate"')).toBe(true);
+  });
+  it("UNKNOWN family stays lenient (a rydberg [system] has no delta; extra leaves ride through)", () => {
+    // No transmon branch fires — only family + gate/T/N are required, family-specific leaves pass.
+    const rydberg = {
+      schema_version: "1",
+      system: { family: "rydberg", Omega_max: 5.0, Delta_max: 10.0, C6: 862690.0, distance: 5.5 },
+      formulation: { gate: "CZ", T: 0.5, N: 40 },
+    };
+    expect(validate(rydberg, "formulation").ok).toBe(true);
+  });
+  it("KNOWN family (transmon) requires its identity leaves: delta/levels/drive_max", () => {
+    for (const leaf of ["delta", "levels", "drive_max"]) {
+      const obj = load("formulation");                       // the valid transmon fixture
+      delete (obj.system as Record<string, unknown>)[leaf];
+      const r = validate(obj, "formulation");
+      expect(r.ok, `transmon missing ${leaf} should reject`).toBe(false);
+      expect(hasErr(r.errors, `/system: missing required key "${leaf}"`)).toBe(true);
+    }
+  });
+  it("transmon leaves are type-checked (levels must be an integer)", () => {
+    const obj = load("formulation");
+    (obj.system as Record<string, unknown>).levels = 3.5;
+    const r = validate(obj, "formulation");
+    expect(r.ok).toBe(false);
+    expect(hasErr(r.errors, "/system/levels")).toBe(true);
+  });
+  it("formulation requires the family-independent core: gate + T + N (Q/R stay optional)", () => {
+    for (const leaf of ["gate", "T", "N"]) {
+      const obj = load("formulation");
+      delete (obj.formulation as Record<string, unknown>)[leaf];
+      const r = validate(obj, "formulation");
+      expect(r.ok, `formulation missing ${leaf} should reject`).toBe(false);
+      expect(hasErr(r.errors, `/formulation: missing required key "${leaf}"`)).toBe(true);
+    }
+    // Q and R absent → still valid (optional per the Slack-agreed shape).
+    const noWeights = load("formulation");
+    delete (noWeights.formulation as Record<string, unknown>).Q;
+    delete (noWeights.formulation as Record<string, unknown>).R;
+    expect(validate(noWeights, "formulation").ok).toBe(true);
+  });
+  it("the invalid fixture (missing family + gate) is rejected", () => {
+    expect(validateFile(join(here, "fixtures", "invalid", "formulation.toml"), "formulation").ok).toBe(false);
+  });
+  it("unknown TOP-LEVEL key is rejected (structure is fixed even though leaves are lenient)", () => {
+    const r = load("formulation"); r.bogus = 1;
+    expect(hasErr(validate(r, "formulation").errors, 'unknown key "bogus"')).toBe(true);
+  });
+});
+
 // ── migration: the contract formalize-don't-fork guarantee (S2) ──
 describe("formalize-don't-fork: real beta.1 artifacts validate under the closed schemas", () => {
   it("a beta.1 manifest (writeManifest shape) + schema_version validates clean", () => {