diff --git a/README.md b/README.md
index e6680e1..87c7c4e 100644
--- a/README.md
+++ b/README.md
@@ -25,11 +25,12 @@ change to the safest sequence that exists, and refuses with a structured
 verdict when it can't prove one (see
 [docs/postgres-online-ddl-reference.md](docs/postgres-online-ddl-reference.md)).
 
-**Status: Phases 1 and 2.1–2.4.** The parse boundary, declarative diff,
-classifier, and router seam are implemented. `pg-sprite migrate --alter '…'`
-runs a bounded optimistic native attempt; routed execution beyond that attempt
-lands in Phase 3. Changes without an available backend get a structured
-refusal (exit code 2). `lint` is still a stub. The design docs and the phased
+**Status: Phases 1 and 2.1–2.5.** The parse boundary, declarative diff,
+classifier, router seam, versioned dry-run plan report, and offline linter
+are implemented. `pg-sprite migrate --alter '…'` runs a bounded optimistic
+native attempt; routed execution beyond that attempt lands in Phase 3.
+Changes without an available backend get a structured refusal (exit code 2).
+The design docs and the phased
 build plan live in [docs/](docs/) — start with
 [docs/README.md](docs/README.md); the vision — what pg-sprite is and is not —
 is [docs/vision.md](docs/vision.md).
diff --git a/SAFETY.md b/SAFETY.md
index ec0a140..da7877c 100644
--- a/SAFETY.md
+++ b/SAFETY.md
@@ -27,9 +27,9 @@ The invariant registry (invariant IDs referenced below) lives in
 | `pkg/checkpoint` — durable resume state | ✅ core | planned (Phase 8) | ST-1, ST-2 |
 | slot lifecycle (in `pkg/decode`) — create, reap, lag ceiling | ✅ core | planned (Phase 8) | ST-3 |
 | `pkg/schemachange` — orchestrator, **cutover swap + fidelity gate** | ✅ core | planned (Phase 7) | LK-2, LK-4, ST-5 |
-| `pkg/statement`, `pkg/planner`, `pkg/schemadiff`, `pkg/router`, `pkg/plan`, `pkg/lint` — classify/diff/route/report | ❌ periphery¹ | `pkg/statement` (parse boundary), `pkg/schemadiff` (introspect/diff via scratch execute-and-introspect), `pkg/planner` (classifier), `pkg/router` (backend assignment + availability policy), and `pkg/plan` (versioned dry-run plan report) exist (Phases 2.1–2.5); `pkg/lint` planned | (CO-7 holds at the parse boundary) |
+| `pkg/statement`, `pkg/planner`, `pkg/schemadiff`, `pkg/router`, `pkg/plan`, `pkg/lint` — classify/diff/route/report | ❌ periphery¹ | `pkg/statement` (parse boundary), `pkg/schemadiff` (introspect/diff via scratch execute-and-introspect), `pkg/planner` (classifier), `pkg/router` (backend assignment + availability policy), `pkg/plan` (versioned dry-run plan report), and `pkg/lint` (offline typed findings) exist (Phases 2.1–2.5) | (CO-7 holds at the parse boundary) |
 | `pkg/verdict` — structured outcome contract, rendering, exit codes | ❌ periphery | exists (Phase 1) | — |
-| `internal/cli` — CLI, flags, help, prompts | ❌ periphery | `migrate`, `status`, `diff`, and `fmt` exist; `lint` is a stub | — |
+| `internal/cli` — CLI, flags, help, prompts | ❌ periphery | `migrate`, `status`, `diff`, `fmt`, and `lint` exist | — |
 | status / progress / advisory rendering, metrics | ❌ periphery | planned | — |
 | orchestrator adapter | ❌ periphery | planned (Phase 11) | OC-* hold *at* the boundary |
 | `internal/testutil` | ❌ test-only | exists | — |
diff --git a/docs/README.md b/docs/README.md
index f37509d..eb80fa6 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -46,6 +46,7 @@ checkpoint/resume, tuned for Aurora. That is the gap this engine targets.
 | [invariants.md](invariants.md) | The canonical **invariant registry** — testable runtime MUST-statements (correctness, locking, state/resume, refusals, orchestration), each with its enforcement point and source. Mined from this doc set plus [Spirit](https://github.com/block/spirit)'s stated safety invariants and [SchemaBot](https://github.com/block/schemabot)'s control-plane discipline; the build plan's phases carry per-invariant test obligations. |
 | [tcb-model.md](tcb-model.md) | The **TCB model** — the trusted-computing-base partition of the engine: which components are the small trusted core that enforces the invariant registry vs the untrusted periphery, the never-trust-callers rule, domain types that make illegal states unrepresentable, the in-TCB engineering rules (from TigerBeetle TIGER_STYLE, s2n-tls, qmail, bitcoin-core), the verification ladder, and the per-side AI-assisted development policy. |
 | [plan-report.md](plan-report.md) | The **plan report contract** — the versioned JSON shape both front doors emit for dry-run plans: fields, closed vocabularies, the fingerprint identity, required consumer behavior for unknown versions/values, and one generated example per source (pinned by test). |
+| [lint-report.md](lint-report.md) | The **lint report contract** — the versioned JSON shape `pg-sprite lint` emits for offline CI gating: finding fields (verbatim SQL, line/column), the codes table, severities and exit behavior, the offline-conservatism rules, and how the contract versions relative to the plan report. |
 | [testing.md](testing.md) | The **test-suite guide** — how to run the suite (unit, per-major, all supported majors, compose database), current coverage, the remaining executor-phase test obligations, and the vanilla-PostgreSQL-matrix vs real-Aurora validation boundary. |
 | [schemabot-integration.md](schemabot-integration.md) | The **single home for orchestrator integration** — how SchemaBot (the reference orchestrator) drives the engine: the pluggable-engine overview, the verb mappings, the concrete adapter contract, and the design constraints (OC-* invariants) the integration imposes on the core. |
 
diff --git a/docs/architecture.md b/docs/architecture.md
index bb4eff8..03a7446 100644
--- a/docs/architecture.md
+++ b/docs/architecture.md
@@ -90,10 +90,10 @@ judged by the same rules regardless of how it arrived:
 | **Introspect** | `pkg/schemadiff` | live catalog (and desired DDL applied to a scratch schema) → schema models | The classifier and diff need *facts*, not text: column types, defaults, and constraint state come from PostgreSQL's own catalog, not a reimplementation of its semantics |
 | **Diff** | `pkg/schemadiff` | desired model vs live model → ordered DDL operations | Declarative mode is a front-end that *produces statements*; its output enters the same pipeline as hand-written DDL, so both modes get identical safety treatment |
 | **Classify** | `pkg/planner` | each operation + introspected facts → native-safe · needs-rewrite · refuse, with the safer native sequence where one exists | The safety decision lives in one pure, testable place — PostgreSQL's missing `ALGORITHM=`/`LOCK=` declaration ([design-principles.md](design-principles.md)) |
-| **Lint** | `pkg/lint` | classified operations → pass or structured refusal | Policy-level rejection of unsafe or unsupported changes *before* any write — separate from the mechanical can-this-run-online judgment |
+| **Lint** | `pkg/lint` | classified operations → typed findings (errors refuse, warnings advise) | Policy-level rejection of unsafe or unsupported changes *before* any write — separate from the mechanical can-this-run-online judgment |
 
-Parse, introspect, diff, and classify exist today (Phases 1–2); lint is the one stage not
-yet built (see the [package map](#package-map) for per-package status).
+All five stages exist today (Phases 1–2.5); see the [package map](#package-map) for
+per-package status.
 
 The planner's verdicts are **requests, not permissions** — executors re-verify their own
 preconditions. Which components are safety-critical (and the stricter rules inside that
@@ -122,8 +122,8 @@ different levels of commitment:
 
 | Package | Role | Status |
 | --- | --- | --- |
-| `cmd/pg-sprite` | CLI entry point (Kong): `migrate` · `diff` · `fmt` · `lint` · `status` | `migrate` · `diff` · `fmt` · `status` exist; `lint` is a stub |
-| `internal/cli` | Command tree and flag handling | `migrate` · `diff` · `fmt` · `status` exist; `lint` is a stub |
+| `cmd/pg-sprite` | CLI entry point (Kong): `migrate` · `diff` · `fmt` · `lint` · `status` | all five exist |
+| `internal/cli` | Command tree and flag handling | all five exist |
 | `internal/testutil` | Test harness: containerized PostgreSQL, throwaway schemas | exists |
 | `pkg/dbconn` | Pool with bounded session timeouts, retries, RDS/Aurora auto-TLS (embedded CA bundle), terminate-blockers; advisory-lock mutual exclusion lands here | exists |
 | `pkg/statement` | `go-pgquery` (Wasm `libpg_query`) parse boundary, typed per-operation descriptors, and advisory rewrites (never hand-parse SQL); migration-time shadow DDL + fingerprints are derived by `pkg/schemadiff` via scratch-DB execute-and-introspect | exists |
@@ -131,7 +131,7 @@ different levels of commitment:
 | `pkg/verdict` | Structured outcome contract (executed / refused + reason + safer idiom), rendering, exit codes | exists (Phase 1) |
 | `pkg/schemadiff` | Execute-and-introspect desired state, introspect the live catalog, and produce an ordered declarative diff | exists |
 | `pkg/planner` | Classify typed operations and emit safer native SQL | exists |
-| `pkg/lint` | Policy-level rejection of unsafe or unsupported operations | planned |
+| `pkg/lint` | Offline lint findings with typed codes: unsupported operations are errors; blocking idioms, rewrites, and destructive drops are warnings | exists (Phase 2.5) |
 | `pkg/plan` | Versioned machine-readable dry-run plan report — the one JSON contract both front doors emit and an orchestrator consumes | exists (Phase 2.5) |
 | `pkg/router` | Route classified statements to native / copy-and-swap / refuse dispositions; copy-and-swap reports unavailable until that backend lands | exists (Phase 2.4) |
 | `pkg/executor` | Bounded optimistic native attempt; the `Executor` contract (`Plan`/`Execute`/`Status`/`Abort`) lands in Phase 3 | bounded optimistic attempt exists |
diff --git a/docs/lint-report.md b/docs/lint-report.md
new file mode 100644
index 0000000..7275a3d
--- /dev/null
+++ b/docs/lint-report.md
@@ -0,0 +1,97 @@
+# The lint report contract
+
+The lint report is the machine-readable result of `pg-sprite lint` — the offline checker
+that runs the same parse-and-classify pipeline as the front doors, with zero live facts and
+no database. It exists so CI can gate a DDL script before any environment sees it. This
+document is the contract: the fields, the closed vocabularies, and the behavior required of
+a consumer. The Go source of truth is `pkg/lint`; tests in `pkg/lint` and `internal/cli` pin
+everything documented here.
+
+## Versioning: `format_version`
+
+Every report carries `format_version`. A consumer that does not recognize the version must
+**reject the report** — never guess at field semantics. The version covers the field shape
+and the closed vocabularies below (codes, severities, and the embedded planner reasons):
+adding a value to any of them is a contract change and bumps `format_version`, even if no
+field is added or renamed.
+
+### Relationship to the plan report
+
+The lint report and the [plan report](plan-report.md) are **versioned independently** — each
+carries its own `format_version`, and they move separately. They share one vocabulary: a
+finding's `reason` draws from the plan report's Reasons set, and the lint `format_version`
+pins the reason set a lint consumer must understand, exactly as the plan `format_version`
+does for plan consumers. A consumer of both must track both versions; understanding plan v1
+says nothing about lint v1.
+
+## Consumer behavior for unknown values
+
+Every enum field draws from a closed vocabulary listed here. A consumer that meets a value
+it does not recognize must **treat the finding as an error and fail the gate** — never
+ignore it and proceed. This mirrors the linter's own posture: an unknown planner route
+becomes an error-severity refusal, never a silent pass.
+
+## Offline conservatism
+
+The linter sees only the script — no catalog, no column types, no server. Every judgment is
+therefore the planner's fail-closed judgment: a change lint passes without findings can
+still sharpen at execution time, but a change lint flags will never quietly get worse. Two
+codes make the conservatism visible instead of burying it:
+
+- `possible-table-rewrite` marks a decision the planner could not verify (see the codes
+  table) — the engine would take the heavy path, but a live database might prove the change
+  free.
+- `destructive` includes every index drop, because the linter cannot see whether an index
+  is unique — and a dropped unique index whose gap admitted duplicate writes cannot be
+  recreated at all.
+
+## Report fields
+
+| Field | Type | Presence | Meaning |
+|---|---|---|---|
+| `format_version` | int | always | Contract version; reject unknown versions. |
+| `postgres_versions` | string | always | The inclusive PostgreSQL major-version range the offline rules are derived for (`14-18`, see [postgresql-version-support.md](postgresql-version-support.md)). The linter never sees a server, so a stored report names the assumptions behind it instead. |
+| `findings` | array | always | The findings in statement order; `[]` (never `null`) means the script is clean. |
+| `errors` | int | always | Count of error-severity findings. |
+| `warnings` | int | always | Count of warning-severity findings. |
+
+## Finding fields
+
+| Field | Type | Presence | Meaning |
+|---|---|---|---|
+| `statement` | int | always | 1-based index of the statement in the script. |
+| `line` | int | always | 1-based source line of the statement's first token, for CI annotations. |
+| `column` | int | always | 1-based source column of the statement's first token. |
+| `sql` | string | always | The statement's **verbatim source text** (without the trailing semicolon), so it can be found in the source by exact match. Unlike the plan report's canonical rendering, a lint finding points back at the file the author wrote. |
+| `operation` | string | always | Operator-facing label of the flagged operation (`DROP COLUMN legacy_a`). Display only — never branch on it. |
+| `code` | string | always | The typed finding kind (see Codes). Automation branches on this, never on prose. |
+| `severity` | string | always | What the engine would do about it (see Severities). |
+| `reason` | string | classifier findings | The planner's typed cause, drawn from the plan report's Reasons vocabulary. Absent for destructive findings, which are a property of the operation, not a routing decision. |
+| `suggestion` | array | when constructible | The ordered safer SQL to run instead, present only for `blocking-idiom` findings where the planner constructed the rewrite. Its absence still means the submitted form blocks — the planner does not construct rewrites for multi-operation statements or for operations that need catalog knowledge (ATTACH PARTITION's proving CHECK). |
+
+## Codes (`code`)
+
+| Value | Severity | Example statement | Meaning |
+|---|---|---|---|
+| `unsupported-operation` | error | `ALTER TABLE t ADD CONSTRAINT x EXCLUDE USING gist (room WITH =)` | No known safe path — the engine refuses it. |
+| `blocking-idiom` | warning | `CREATE INDEX i ON t (c)` | The submitted form blocks readers or writers and a safer native form exists; `suggestion` carries it when the linter can construct one. |
+| `table-rewrite` | warning | `ALTER TABLE t ALTER COLUMN c TYPE jsonb USING c::jsonb` | The operation provably rewrites the table — only the engine's copy-and-swap path can run it online. |
+| `possible-table-rewrite` | warning | `ALTER TABLE t ALTER COLUMN c TYPE bigint` | The linter cannot verify the operation against live column facts, so the engine would fail closed to the rewrite path — but the change may be a free relabel a live database would prove. |
+| `destructive` | warning | `ALTER TABLE t DROP COLUMN legacy` | The operation discards live structure (a column, constraint, or index drop) and cannot be undone by re-running the schema. |
+
+## Severities (`severity`)
+
+| Value | Meaning | Exit behavior |
+|---|---|---|
+| `error` | The engine would refuse the statement — it cannot execute as written. | `pg-sprite lint` exits non-zero. |
+| `warning` | The engine would execute the statement, but it has a safer form, needs a heavier path, or discards live structure. | Warnings alone exit zero. |
+
+Only error-severity findings flip the exit code today; a policy layer (per-code gating,
+inline suppression) is a planned extension and will be introduced as a contract change.
+
+## Text output
+
+Without `--json`, findings render one per line in the conventional linter shape —
+`name:line:column: severity: code — operation` — where `name` is the linted file path or
+`<stdin>`. The text form is for humans and editors; automation consumes the JSON report.
+A clean script prints nothing and exits zero.
diff --git a/docs/low-level-design.md b/docs/low-level-design.md
index 4df8767..14a511f 100644
--- a/docs/low-level-design.md
+++ b/docs/low-level-design.md
@@ -80,7 +80,7 @@ seam inside the copy-and-swap executor is the same idea applied one level down.
    │  pkg/statement   parse ALTER/CREATE (go-pgquery)                           │
    │  pkg/schemadiff  introspect live schema → diff vs desired → ordered ALTERs │
    │  pkg/planner     per op: native-safe | needs-rewrite | refuse              │
-   │  pkg/lint        reject unsafe/unsupported up front (planned)              │
+   │  pkg/lint        reject unsafe/unsupported up front (offline findings)     │
    │      │                                                                     │
    │      ▼  Plan (ordered steps, classified per operation)                     │
    └──────┬─────────────────────────────────────────────────────────────────────┘
@@ -177,8 +177,8 @@ pattern *per migration*:
 - **expand/contract via pgroll** for prod-critical breaking changes where **instant
   reversibility** and **two live schema versions** matter more than transparency.
 
-The classifier, declarative diff, dry-run, and status reporting are shared by every backend;
-linting remains planned. An `Executor` interface (`Plan`, `Execute`, `Status`, `Abort`) is also
+The classifier, declarative diff, dry-run, lint, and status reporting are shared by every
+backend. An `Executor` interface (`Plan`, `Execute`, `Status`, `Abort`) is also
 planned; `pkg/executor` currently provides only the bounded optimistic native attempt. Until the
 in-house copy-and-swap executor
 lands in a later phase, every `needs-rewrite` change is refused as **not native-safe** rather than
@@ -318,13 +318,13 @@ For each parsed statement the classifier produces a record along the lines of:
 - Richer `risk`, `reversible`, and `requires_app_coordination` metadata is a future extension.
 
 Classification belongs to `pkg/planner`; `pkg/statement` supplies typed operations and
-`pkg/lint` remains a stub.
+`pkg/lint` maps the classifier's decisions to offline findings with typed codes.
 
 ### CLI behaviour (modes)
 
 | Invocation | Behaviour |
 | --- | --- |
-| `lint` | Stub; no lint engine is implemented yet. |
+| `lint` | Offline (no database): classify every statement with zero live facts and report typed findings — unsupported operations are errors (non-zero exit), blocking idioms (with the safer SQL), conservative rewrites, and destructive drops are warnings. |
 | `diff` / `migrate --dry-run` | Print the classified, routed plan and safer SQL where applicable. **Never executes.** `diff` has no `--dry-run` flag because it never executes. |
 | `migrate` (default) | Run the Phase 1 statement gate, preflight, and bounded optimistic native attempt. It does not yet execute classifier-produced safer SQL. |
 | `migrate --force` (planned Phase 3) | Run each statement **exactly as submitted**, bypassing the safe rewrite. Gated — see below. |
@@ -600,13 +600,13 @@ pkg/schemadiff/       -> execute-and-introspect desired state + live introspecti
 pkg/planner/          -> classify each operation and construct safer native SQL
 pkg/router/           -> assign classified statements to available backends
 pkg/plan/             -> versioned machine-readable dry-run plan report (both front doors)
+pkg/lint/             -> offline typed lint findings (errors refuse, warnings advise)
 pkg/executor/         -> bounded optimistic native attempt only
 pkg/dbconn/           -> bounded database connections
 pkg/preflight/        -> migration preflight checks
 pkg/verdict/          -> typed outcomes
 
 Planned:
-pkg/lint/             -> unsafe-DDL linters (currently a CLI stub)
 pkg/migration/        -> orchestrator + runner + cutover
 pkg/decode/           -> logical-decoding client
 pkg/copier/           -> parallel chunked copy
diff --git a/docs/plan-report.md b/docs/plan-report.md
index fb2afa5..a1abf85 100644
--- a/docs/plan-report.md
+++ b/docs/plan-report.md
@@ -17,6 +17,10 @@ kinds) and the fingerprint serialization are all pinned to it. Adding a vocabula
 changing the fingerprint definition is a contract change and bumps `format_version`, even if
 no field is added or renamed.
 
+The [lint report](lint-report.md) is a separate contract with its own `format_version`; the
+two version independently. Lint findings embed this contract's Reasons vocabulary — the lint
+`format_version` pins the reason set for lint consumers, as this one does for plan consumers.
+
 ## Consumer behavior for unknown values
 
 Every enum field in the report draws from a closed vocabulary listed here. A consumer that
@@ -59,6 +63,7 @@ with SQL it does not fully understand.
 | `destructive` | bool | always | Whether this operation discards live structure. Always emitted, never omitted. |
 | `route` | string | always | Where the operation goes (see Routes). |
 | `reason` | string | always | The typed cause of the routing decision (see Reasons). Automation branches on this, never on prose. |
+| `unverified` | bool | when true | The planner failed closed to this route for lack of live facts — the route is what the engine would do, not a proven property of the change. With facts (a live introspection or a supplied column type) the same operation may classify as native. Absent means the decision is proven. |
 | `safer_sql` | array | safer-idiom only | The ordered native sequence to run instead of the submitted form, when the planner could construct it. |
 
 ## Closed vocabularies
diff --git a/docs/testing.md b/docs/testing.md
index b15e9f1..b45f0a2 100644
--- a/docs/testing.md
+++ b/docs/testing.md
@@ -174,6 +174,8 @@ this repository's CI.
 | Native / copy-and-swap / refuse classification and safer SQL | [pkg/planner](../pkg/planner/planner_test.go) |
 | Backend routing and copy-and-swap unavailable disposition | [pkg/router](../pkg/router/router_test.go) |
 | Plan report contract: exact JSON shape, versioning, field omissions | [pkg/plan](../pkg/plan/plan_test.go) |
+| Offline lint findings: typed codes, severities, counts, JSON contract; CLI exit contract | [pkg/lint](../pkg/lint/lint_test.go), [CLI lint](../internal/cli/lint_test.go) |
+| Script splitting through the grammar (canonical statements, parse failures) | [pkg/statement](../pkg/statement/split_test.go) |
 | Scratch execute-and-introspect, ordered diff, and convergence (`TestDiffConverges`) | [pkg/schemadiff](../pkg/schemadiff/schemadiff_integration_test.go), [diff tests](../pkg/schemadiff/diff_test.go) |
 | CLI `diff`, `fmt`, and classified `migrate --dry-run`, including applying text output and re-diffing to empty (`TestDiffTextPlanIsExecutableSQL`) | [diff integration](../internal/cli/diff_integration_test.go), [fmt](../internal/cli/diff_test.go), [dry-run integration](../internal/cli/dryrun_integration_test.go) |
 | Bounded optimistic native attempt and table preflight | [pkg/executor](../pkg/executor/optimistic_integration_test.go), [pkg/preflight](../pkg/preflight/preflight_integration_test.go) |
diff --git a/internal/cli/cli.go b/internal/cli/cli.go
index 24a14da..99caf57 100644
--- a/internal/cli/cli.go
+++ b/internal/cli/cli.go
@@ -1,6 +1,6 @@
-// Package cli defines the pg-sprite command tree (Kong). migrate and status
-// are implemented (the Phase 1 optimistic front door); the remaining
-// subcommand Run methods are stubs each build-plan phase fills in.
+// Package cli defines the pg-sprite command tree (Kong): migrate and
+// status (the optimistic front door), diff and fmt (the declarative front
+// door), and lint (the offline checker).
 package cli
 
 import (
@@ -31,10 +31,6 @@ type CLI struct {
 // New returns an empty command tree for kong.Parse.
 func New() *CLI { return &CLI{} }
 
-func notImplemented(cmd string) error {
-	return fmt.Errorf("%s: not implemented yet (Phase 0 stub)", cmd)
-}
-
 // DBFlags are the connection flags shared by every command that talks to the
 // database, so every entry point carries the same bounded session defaults.
 type DBFlags struct {
@@ -128,11 +124,15 @@ type FmtCmd struct {
 // Run implements the fmt subcommand.
 func (c *FmtCmd) Run() error { return c.runFmt(os.Stdin, os.Stdout) }
 
-// LintCmd checks DDL for unsafe or unsupported patterns.
-type LintCmd struct{}
+// LintCmd checks a DDL script for patterns the engine would refuse,
+// rewrite, or gate. It is offline — no database flags.
+type LintCmd struct {
+	Path string `arg:"" optional:"" help:"DDL file to lint; stdin when omitted." type:"existingfile"`
+	JSON bool   `help:"Emit the findings report as JSON."`
+}
 
 // Run implements the lint subcommand.
-func (c *LintCmd) Run() error { return notImplemented("lint") }
+func (c *LintCmd) Run() error { return c.runLint(os.Stdin, os.Stdout) }
 
 // StatusCmd reports schema-change progress.
 type StatusCmd struct {
diff --git a/internal/cli/lint.go b/internal/cli/lint.go
new file mode 100644
index 0000000..1f31d1a
--- /dev/null
+++ b/internal/cli/lint.go
@@ -0,0 +1,77 @@
+package cli
+
+import (
+	"encoding/json"
+	"errors"
+	"fmt"
+	"io"
+	"os"
+	"strings"
+
+	"github.com/block/pg-sprite/pkg/lint"
+)
+
+// ErrLintFindings is returned by lint when the script has error-severity
+// findings, so the process exits non-zero; warnings alone pass.
+var ErrLintFindings = errors.New("lint found errors")
+
+// runLint lints a DDL script: parse every statement through the PostgreSQL
+// grammar, classify it with zero live facts, and report typed findings.
+// Offline — no database. A clean script prints nothing.
+func (c *LintCmd) runLint(in io.Reader, out io.Writer) error {
+	var src []byte
+	var err error
+	if c.Path == "" {
+		if src, err = io.ReadAll(in); err != nil {
+			return fmt.Errorf("read DDL from stdin: %w", err)
+		}
+	} else if src, err = os.ReadFile(c.Path); err != nil {
+		return fmt.Errorf("read DDL file: %w", err)
+	}
+	report, err := lint.Check(string(src))
+	if err != nil {
+		return err
+	}
+	if c.JSON {
+		enc := json.NewEncoder(out)
+		enc.SetIndent("", "  ")
+		if err := enc.Encode(report); err != nil {
+			return fmt.Errorf("write lint report: %w", err)
+		}
+	} else if err := writeLintText(out, c.sourceName(), report); err != nil {
+		return err
+	}
+	if report.Errors > 0 {
+		return fmt.Errorf("%w: %d", ErrLintFindings, report.Errors)
+	}
+	return nil
+}
+
+// sourceName names the linted source for text findings: the file path, or
+// the conventional "<stdin>" when the script came from the pipe.
+func (c *LintCmd) sourceName() string {
+	if c.Path == "" {
+		return "<stdin>"
+	}
+	return c.Path
+}
+
+// writeLintText renders the findings in the conventional linter shape —
+// name:line:column: severity — one per line with any suggestion indented
+// beneath it, so CI systems and editors can jump to the source. A clean
+// report prints nothing.
+func writeLintText(out io.Writer, name string, report lint.Report) error {
+	for _, f := range report.Findings {
+		if _, err := fmt.Fprintf(out, "%s:%d:%d: %s: %s — %s\n",
+			name, f.Line, f.Column, f.Severity, f.Code, f.Operation); err != nil {
+			return fmt.Errorf("write lint report: %w", err)
+		}
+		if len(f.Suggestion) > 0 {
+			if _, err := fmt.Fprintf(out, "  run instead: %s;\n",
+				strings.Join(f.Suggestion, ";\n  ")); err != nil {
+				return fmt.Errorf("write lint report: %w", err)
+			}
+		}
+	}
+	return nil
+}
diff --git a/internal/cli/lint_test.go b/internal/cli/lint_test.go
new file mode 100644
index 0000000..242537e
--- /dev/null
+++ b/internal/cli/lint_test.go
@@ -0,0 +1,81 @@
+package cli
+
+import (
+	"encoding/json"
+	"os"
+	"path/filepath"
+	"strings"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+	"github.com/stretchr/testify/require"
+
+	"github.com/block/pg-sprite/pkg/lint"
+)
+
+func TestLintCleanScriptPrintsNothing(t *testing.T) {
+	var out strings.Builder
+	cmd := LintCmd{}
+	err := cmd.runLint(strings.NewReader("CREATE TABLE t (id int)"), &out)
+	require.NoError(t, err)
+	assert.Empty(t, out.String())
+}
+
+// Warning findings are reported but do not fail the command; only
+// error-severity findings flip the exit code.
+func TestLintWarningsPassErrorsFail(t *testing.T) {
+	var out strings.Builder
+	cmd := LintCmd{JSON: true}
+	err := cmd.runLint(strings.NewReader("CREATE INDEX t_c_idx ON t (c)"), &out)
+	require.NoError(t, err)
+
+	out.Reset()
+	err = cmd.runLint(strings.NewReader(
+		"ALTER TABLE t ADD CONSTRAINT no_overlap EXCLUDE USING gist (room WITH =)"), &out)
+	require.ErrorIs(t, err, ErrLintFindings)
+
+	var report lint.Report
+	require.NoError(t, json.Unmarshal([]byte(out.String()), &report))
+	assert.Equal(t, lint.FormatVersion, report.FormatVersion)
+	assert.Equal(t, 1, report.Errors)
+	require.Len(t, report.Findings, 1)
+	assert.Equal(t, lint.CodeUnsupportedOperation, report.Findings[0].Code)
+}
+
+func TestLintReadsFromFile(t *testing.T) {
+	path := filepath.Join(t.TempDir(), "change.sql")
+	require.NoError(t, os.WriteFile(path,
+		[]byte("ALTER TABLE t DROP COLUMN legacy"), 0o600))
+
+	var out strings.Builder
+	cmd := LintCmd{Path: path, JSON: true}
+	require.NoError(t, cmd.runLint(strings.NewReader(""), &out))
+
+	var report lint.Report
+	require.NoError(t, json.Unmarshal([]byte(out.String()), &report))
+	require.Len(t, report.Findings, 1)
+	assert.Equal(t, lint.CodeDestructive, report.Findings[0].Code)
+	assert.Equal(t, 1, report.Warnings)
+}
+
+// The text renderer emits the conventional name:line:column: shape so CI
+// systems and editors can jump to the finding. This is the renderer's own
+// unit test — everything else asserts typed fields.
+func TestLintTextFindingsCarryPositions(t *testing.T) {
+	var out strings.Builder
+	cmd := LintCmd{}
+	err := cmd.runLint(strings.NewReader(
+		"CREATE TABLE ok (id int);\nALTER TABLE t DROP COLUMN legacy;\n"), &out)
+	require.NoError(t, err)
+	assert.Equal(t,
+		"<stdin>:2:1: warning: destructive — DROP COLUMN legacy\n",
+		out.String())
+}
+
+func TestLintParseFailureIsErrorNotFinding(t *testing.T) {
+	var out strings.Builder
+	cmd := LintCmd{}
+	err := cmd.runLint(strings.NewReader("CREATE TABEL t (id int)"), &out)
+	require.Error(t, err)
+	assert.NotErrorIs(t, err, ErrLintFindings)
+}
diff --git a/pkg/lint/lint.go b/pkg/lint/lint.go
new file mode 100644
index 0000000..7ba7641
--- /dev/null
+++ b/pkg/lint/lint.go
@@ -0,0 +1,203 @@
+// Package lint checks DDL offline for patterns the engine would refuse,
+// rewrite, or gate. It runs the same parse-and-classify pipeline as the
+// front doors but with zero live facts, so it needs no database and is
+// strictly conservative: a change lint passes without findings can still
+// sharpen at execution time, but a change lint flags will never quietly
+// get worse. Findings carry typed codes automation branches on — never
+// prose.
+package lint
+
+import (
+	"fmt"
+
+	"github.com/block/pg-sprite/pkg/planner"
+	"github.com/block/pg-sprite/pkg/statement"
+)
+
+// FormatVersion identifies the report contract. A consumer must reject a
+// report whose version it does not understand instead of guessing at the
+// field semantics.
+const FormatVersion = 1
+
+// Severity ranks a finding by what the engine would do with it.
+type Severity string
+
+// The severities a finding can carry.
+const (
+	// SeverityError: the engine would refuse the statement — it cannot
+	// execute as written.
+	SeverityError Severity = "error"
+	// SeverityWarning: the engine would execute the statement, but it has
+	// a safer form, needs a heavier path, or discards live structure.
+	SeverityWarning Severity = "warning"
+)
+
+// Code is the typed finding kind; automation branches on it, never on
+// prose.
+type Code string
+
+// The finding codes.
+const (
+	// CodeUnsupportedOperation: no known safe path — the engine refuses it.
+	CodeUnsupportedOperation Code = "unsupported-operation"
+	// CodeBlockingIdiom: the submitted form blocks readers or writers and
+	// a safer native form exists; Suggestion carries it when the linter
+	// can construct one.
+	CodeBlockingIdiom Code = "blocking-idiom"
+	// CodeTableRewrite: the operation needs a full table rewrite — only
+	// the engine's copy-and-swap path can run it online. Reason carries
+	// the specific cause.
+	CodeTableRewrite Code = "table-rewrite"
+	// CodePossibleTableRewrite: the linter cannot verify the operation
+	// against live column facts, so the engine would fail closed to the
+	// rewrite path — but the change may be a free relabel that a live
+	// database would prove. The route is what the engine would do, not a
+	// proven property of the change.
+	CodePossibleTableRewrite Code = "possible-table-rewrite"
+	// CodeDestructive: the operation discards live structure (a column,
+	// constraint, or index drop) and cannot be undone by re-running the
+	// schema. Index drops are included because the linter cannot see
+	// whether an index is unique — and a dropped unique index whose gap
+	// admitted duplicates cannot be recreated at all.
+	CodeDestructive Code = "destructive"
+)
+
+// Finding is one lint result: the statement it is about, the typed code,
+// and the severity.
+type Finding struct {
+	// Statement is the 1-based index of the statement in the script.
+	Statement int `json:"statement"`
+	// Line is the 1-based source line of the statement's first token, so
+	// a CI system can annotate the finding onto the file it came from.
+	Line int `json:"line"`
+	// Column is the 1-based source column of the statement's first token.
+	Column int `json:"column"`
+	// SQL is the verbatim source text of that statement, so it can be
+	// found in the source by exact match.
+	SQL string `json:"sql"`
+	// Operation is the operator-facing label of the flagged operation
+	// (display only).
+	Operation string `json:"operation"`
+	// Code is the typed finding kind.
+	Code Code `json:"code"`
+	// Severity is what the engine would do about it.
+	Severity Severity `json:"severity"`
+	// Reason is the classifier's typed cause, present for findings the
+	// classifier produced (blocking-idiom, table-rewrite, unsupported).
+	Reason planner.Reason `json:"reason,omitempty"`
+	// Suggestion is the ordered safer SQL to run instead, present only
+	// for blocking-idiom findings where the linter could construct it.
+	Suggestion []string `json:"suggestion,omitempty"`
+}
+
+// Report is the lint result for one script.
+type Report struct {
+	// FormatVersion is the report contract version; always FormatVersion.
+	FormatVersion int `json:"format_version"`
+	// PostgresVersions is the inclusive PostgreSQL major-version range
+	// the offline rules are derived for (planner.RulesPostgresVersions).
+	// The linter never sees a server, so a stored report names the
+	// assumptions behind it instead.
+	PostgresVersions string `json:"postgres_versions"`
+	// Findings are the results in statement order; empty means the script
+	// is clean.
+	Findings []Finding `json:"findings"`
+	// Errors counts error-severity findings.
+	Errors int `json:"errors"`
+	// Warnings counts warning-severity findings.
+	Warnings int `json:"warnings"`
+}
+
+// Check lints a DDL script: every statement is parsed with the PostgreSQL
+// grammar and classified with zero live facts. A parse failure is an
+// error; an unsupported operation is not — it is an error-severity
+// finding, so one bad statement never hides the rest of the report.
+func Check(sql string) (Report, error) {
+	stmts, err := statement.Split(sql)
+	if err != nil {
+		return Report{}, err
+	}
+	report := Report{
+		FormatVersion:    FormatVersion,
+		PostgresVersions: planner.RulesPostgresVersions,
+		Findings:         []Finding{},
+	}
+	for i, stmt := range stmts {
+		findings, err := checkStatement(i+1, stmt)
+		if err != nil {
+			return Report{}, fmt.Errorf("statement %d: %w", i+1, err)
+		}
+		report.Findings = append(report.Findings, findings...)
+	}
+	for _, f := range report.Findings {
+		if f.Severity == SeverityError {
+			report.Errors++
+		} else {
+			report.Warnings++
+		}
+	}
+	return report, nil
+}
+
+// checkStatement produces the findings for one statement, all derived
+// from the classifier's routing decisions: a routing finding where the
+// route warrants one, and a destructive finding where the decision is
+// marked destructive. The classifier is the single rulebook — the linter
+// adds severity and presentation, never a second opinion.
+func checkStatement(index int, stmt statement.SourceStatement) ([]Finding, error) {
+	classified, err := planner.Classify(stmt.SQL, planner.Facts{})
+	if err != nil {
+		return nil, err
+	}
+	var findings []Finding
+	place := func(f Finding) Finding {
+		f.Statement, f.Line, f.Column, f.SQL = index, stmt.Line, stmt.Column, stmt.SQL
+		return f
+	}
+	for _, d := range classified.Decisions {
+		if f, flagged := decisionFinding(d); flagged {
+			findings = append(findings, place(f))
+		}
+		if d.Destructive {
+			findings = append(findings, place(Finding{
+				Operation: d.Operation,
+				Code:      CodeDestructive,
+				Severity:  SeverityWarning,
+			}))
+		}
+	}
+	return findings, nil
+}
+
+// decisionFinding maps one routing decision to its finding. Decisions that
+// are already the safe native form produce no finding.
+func decisionFinding(d planner.Decision) (Finding, bool) {
+	f := Finding{Operation: d.Operation, Reason: d.Reason}
+	switch d.Route {
+	case planner.RouteRefuse:
+		f.Code, f.Severity = CodeUnsupportedOperation, SeverityError
+		return f, true
+	case planner.RouteCopyAndSwap:
+		if d.Unverified {
+			// The planner failed closed for lack of facts: report "the
+			// engine would take the heavy path", not "this rewrites the
+			// table" — only the second is a property of the change.
+			f.Code, f.Severity = CodePossibleTableRewrite, SeverityWarning
+			return f, true
+		}
+		f.Code, f.Severity = CodeTableRewrite, SeverityWarning
+		return f, true
+	case planner.RouteNative:
+		if d.Reason == planner.ReasonSaferIdiom {
+			f.Code, f.Severity = CodeBlockingIdiom, SeverityWarning
+			f.Suggestion = d.SaferSQL
+			return f, true
+		}
+		return Finding{}, false
+	default:
+		// An unknown route is a planner contract violation; fail closed
+		// as a refusal rather than passing it silently.
+		f.Code, f.Severity = CodeUnsupportedOperation, SeverityError
+		return f, true
+	}
+}
diff --git a/pkg/lint/lint_test.go b/pkg/lint/lint_test.go
new file mode 100644
index 0000000..f7e8920
--- /dev/null
+++ b/pkg/lint/lint_test.go
@@ -0,0 +1,193 @@
+package lint_test
+
+import (
+	"encoding/json"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+	"github.com/stretchr/testify/require"
+
+	"github.com/block/pg-sprite/pkg/lint"
+	"github.com/block/pg-sprite/pkg/planner"
+)
+
+func TestCheckCleanScriptHasNoFindings(t *testing.T) {
+	report, err := lint.Check(`
+		CREATE TABLE t (id bigint PRIMARY KEY);
+		ALTER TABLE t ADD COLUMN age int DEFAULT 0;
+		CREATE INDEX CONCURRENTLY t_age_idx ON t (age);
+	`)
+	require.NoError(t, err)
+	assert.Equal(t, lint.FormatVersion, report.FormatVersion)
+	assert.Equal(t, planner.RulesPostgresVersions, report.PostgresVersions)
+	assert.Empty(t, report.Findings)
+	assert.Zero(t, report.Errors)
+	assert.Zero(t, report.Warnings)
+}
+
+func TestCheckEmptyScriptIsClean(t *testing.T) {
+	report, err := lint.Check("")
+	require.NoError(t, err)
+	assert.Empty(t, report.Findings)
+}
+
+func TestCheckParseFailureIsError(t *testing.T) {
+	_, err := lint.Check("ALTER TABEL t ADD COLUMN c int")
+	require.Error(t, err)
+}
+
+func TestCheckFlagsBlockingIdiomWithSuggestion(t *testing.T) {
+	report, err := lint.Check("CREATE INDEX t_c_idx ON t (c)")
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 1)
+	f := report.Findings[0]
+	assert.Equal(t, 1, f.Statement)
+	assert.Equal(t, lint.CodeBlockingIdiom, f.Code)
+	assert.Equal(t, lint.SeverityWarning, f.Severity)
+	assert.Equal(t, planner.ReasonSaferIdiom, f.Reason)
+	require.Len(t, f.Suggestion, 1)
+	assert.NotEqual(t, f.SQL, f.Suggestion[0], "the suggestion is the concurrent rewrite")
+	assert.Equal(t, 0, report.Errors)
+	assert.Equal(t, 1, report.Warnings)
+}
+
+// With zero live facts a type change is not provably a rewrite — the
+// engine would fail closed to the heavy path, and the finding says that
+// rather than asserting a property of the change the linter cannot know.
+func TestCheckFlagsUnverifiedTypeChangeAsPossibleRewrite(t *testing.T) {
+	report, err := lint.Check("ALTER TABLE t ALTER COLUMN id TYPE bigint")
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 1)
+	f := report.Findings[0]
+	assert.Equal(t, lint.CodePossibleTableRewrite, f.Code)
+	assert.Equal(t, lint.SeverityWarning, f.Severity)
+	assert.Equal(t, planner.ReasonTypeRewrite, f.Reason)
+}
+
+// A USING clause is a rewrite regardless of live facts, so the finding is
+// the proven code, not the fail-closed one.
+func TestCheckFlagsProvenRewriteAsTableRewrite(t *testing.T) {
+	report, err := lint.Check("ALTER TABLE t ALTER COLUMN id TYPE integer USING id::integer")
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 1)
+	f := report.Findings[0]
+	assert.Equal(t, lint.CodeTableRewrite, f.Code)
+	assert.Equal(t, planner.ReasonTypeRewrite, f.Reason)
+}
+
+func TestCheckFlagsUnsupportedAsError(t *testing.T) {
+	report, err := lint.Check(
+		"ALTER TABLE t ADD CONSTRAINT no_overlap EXCLUDE USING gist (room WITH =)")
+	require.NoError(t, err, "an unsupported operation is a finding, not a lint failure")
+	require.Len(t, report.Findings, 1)
+	f := report.Findings[0]
+	assert.Equal(t, lint.CodeUnsupportedOperation, f.Code)
+	assert.Equal(t, lint.SeverityError, f.Severity)
+	assert.Equal(t, planner.ReasonUnsupportedOperation, f.Reason)
+	assert.Equal(t, 1, report.Errors)
+	assert.Equal(t, 0, report.Warnings)
+}
+
+// Destructive findings come from the classifier's destructive flag, so
+// the linter and the plan report mark the same operations by
+// construction. Index drops are destructive even in the concurrent form:
+// offline the linter cannot see whether the index is unique, and a
+// dropped unique index is not recreatable once writes exploit the gap.
+func TestCheckFlagsDestructiveDrops(t *testing.T) {
+	report, err := lint.Check(`
+		ALTER TABLE t DROP COLUMN legacy;
+		ALTER TABLE t DROP CONSTRAINT t_check;
+		DROP INDEX CONCURRENTLY t_c_idx;
+	`)
+	require.NoError(t, err)
+	var codes []lint.Code
+	var stmts []int
+	for _, f := range report.Findings {
+		codes = append(codes, f.Code)
+		stmts = append(stmts, f.Statement)
+	}
+	assert.Equal(t, []lint.Code{
+		lint.CodeDestructive, lint.CodeDestructive, lint.CodeDestructive,
+	}, codes)
+	assert.Equal(t, []int{1, 2, 3}, stmts)
+}
+
+// A multi-operation statement can produce several findings, and finding
+// indexes track the statement, not the finding count.
+func TestCheckMultiStatementMultiFinding(t *testing.T) {
+	report, err := lint.Check(`
+		ALTER TABLE t DROP COLUMN legacy, ALTER COLUMN id TYPE bigint;
+		CREATE INDEX t_c_idx ON t (c);
+	`)
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 3)
+	assert.Equal(t, lint.CodeDestructive, report.Findings[0].Code)
+	assert.Equal(t, 1, report.Findings[0].Statement)
+	assert.Equal(t, lint.CodePossibleTableRewrite, report.Findings[1].Code)
+	assert.Equal(t, 1, report.Findings[1].Statement)
+	assert.Equal(t, lint.CodeBlockingIdiom, report.Findings[2].Code)
+	assert.Equal(t, 2, report.Findings[2].Statement)
+	assert.Equal(t, 0, report.Errors)
+	assert.Equal(t, 3, report.Warnings)
+}
+
+// Findings carry the statement's verbatim source text and its position,
+// so a CI system can annotate the file and a reader can find the text by
+// exact match.
+func TestCheckFindingsCarrySourcePositions(t *testing.T) {
+	report, err := lint.Check(
+		"CREATE TABLE ok (id int);\n\n\n\n\nALTER TABLE t DROP COLUMN legacy_a;\n")
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 1)
+	f := report.Findings[0]
+	assert.Equal(t, 2, f.Statement)
+	assert.Equal(t, 6, f.Line)
+	assert.Equal(t, 1, f.Column)
+	assert.Equal(t, "ALTER TABLE t DROP COLUMN legacy_a", f.SQL,
+		"verbatim source, not a canonical reprint")
+}
+
+// The JSON shape is the automation-facing contract: exact keys, exact
+// omissions, findings as [] when clean.
+func TestReportJSONShape(t *testing.T) {
+	report, err := lint.Check("ALTER TABLE t ALTER COLUMN c SET NOT NULL")
+	require.NoError(t, err)
+	raw, err := json.Marshal(report)
+	require.NoError(t, err)
+	require.Len(t, report.Findings, 1)
+	suggestion, err := json.Marshal(report.Findings[0].Suggestion)
+	require.NoError(t, err)
+	assert.JSONEq(t, `{
+		"format_version": 1,
+		"postgres_versions": "14-18",
+		"findings": [
+			{
+				"statement": 1,
+				"line": 1,
+				"column": 1,
+				"sql": "ALTER TABLE t ALTER COLUMN c SET NOT NULL",
+				"operation": "ALTER COLUMN c SET NOT NULL",
+				"code": "blocking-idiom",
+				"severity": "warning",
+				"reason": "safer-idiom",
+				"suggestion": `+string(suggestion)+`
+			}
+		],
+		"errors": 0,
+		"warnings": 1
+	}`, string(raw))
+}
+
+func TestReportJSONCleanFindingsAreEmptyArray(t *testing.T) {
+	report, err := lint.Check("CREATE TABLE t (id int)")
+	require.NoError(t, err)
+	raw, err := json.Marshal(report)
+	require.NoError(t, err)
+	assert.JSONEq(t, `{
+		"format_version": 1,
+		"postgres_versions": "14-18",
+		"findings": [],
+		"errors": 0,
+		"warnings": 0
+	}`, string(raw))
+}
diff --git a/pkg/planner/planner.go b/pkg/planner/planner.go
index 46c635c..63a4796 100644
--- a/pkg/planner/planner.go
+++ b/pkg/planner/planner.go
@@ -34,6 +34,13 @@ import (
 	"github.com/block/pg-sprite/pkg/statement"
 )
 
+// RulesPostgresVersions is the inclusive PostgreSQL major-version range
+// the classification rules are derived for (see the package comment and
+// docs/postgresql-version-support.md). Offline consumers such as the
+// linter stamp it into their reports so a stored result names the
+// assumptions behind it.
+const RulesPostgresVersions = "14-18"
+
 // Route is where an operation is sent.
 type Route string
 
@@ -143,6 +150,12 @@ type Decision struct {
 	Route Route `json:"route"`
 	// Reason is why.
 	Reason Reason `json:"reason"`
+	// Unverified marks a decision the planner took without the live facts
+	// needed to prove a cheaper one — it failed closed to the heavier
+	// route. The route is what the engine would do, not a proven property
+	// of the change: with facts (a live introspection or a supplied
+	// column type) the same operation may classify as native.
+	Unverified bool `json:"unverified,omitempty"`
 	// SaferSQL is the ordered native sequence to run instead of the
 	// submitted form, present only for safer-idiom decisions where the
 	// planner could construct it. Execution contract: the steps run one at
@@ -256,7 +269,7 @@ func classifyOp(op statement.Op, st statement.Statement, facts Facts, sql string
 		d.Route, d.Reason = RouteNative, ReasonMetadataOnly
 
 	case statement.OpAlterColumnType:
-		d.Route, d.Reason = classifyTypeChange(op, facts)
+		d.Route, d.Reason, d.Unverified = classifyTypeChange(op, facts)
 
 	case statement.OpSetNotNull:
 		// Native pattern: prove the invariant with a NOT VALID CHECK plus
@@ -368,18 +381,21 @@ func classifyAddConstraint(op statement.Op, st statement.Statement, sql string,
 // classifyTypeChange routes ALTER COLUMN TYPE: binary-coercible changes are
 // a brief catalog relabel; everything else — or anything the planner cannot
 // verify against live column facts — is a rewrite.
-func classifyTypeChange(op statement.Op, facts Facts) (Route, Reason) {
+func classifyTypeChange(op statement.Op, facts Facts) (Route, Reason, bool) {
 	if op.HasUsing {
-		return RouteCopyAndSwap, ReasonTypeRewrite
+		return RouteCopyAndSwap, ReasonTypeRewrite, false
 	}
 	oldType, ok := facts.ColumnTypes[op.Column]
 	if !ok {
-		return RouteCopyAndSwap, ReasonTypeRewrite
+		// No live type for the column: fail closed to the rewrite route,
+		// but say so — the conversion may be a free relabel that a fact
+		// would prove.
+		return RouteCopyAndSwap, ReasonTypeRewrite, true
 	}
 	if binaryCoercible(parseTypeText(oldType), typeShape{name: normalizeTypeName(op.NewType), mods: op.NewTypeMods}) {
-		return RouteNative, ReasonBinaryCoercible
+		return RouteNative, ReasonBinaryCoercible, false
 	}
-	return RouteCopyAndSwap, ReasonTypeRewrite
+	return RouteCopyAndSwap, ReasonTypeRewrite, false
 }
 
 // typeShape is a normalized type family plus its modifiers, comparable
diff --git a/pkg/planner/planner_test.go b/pkg/planner/planner_test.go
index be55f2c..c990a4c 100644
--- a/pkg/planner/planner_test.go
+++ b/pkg/planner/planner_test.go
@@ -58,6 +58,34 @@ func TestClassifyMarksDropsDestructive(t *testing.T) {
 	}
 }
 
+// Unverified separates "the planner proved a rewrite" from "the planner
+// failed closed for lack of facts": the same conversion is a proven
+// relabel with a column fact, and an unverified rewrite without one. A
+// USING clause is a rewrite regardless of facts, so it is never
+// unverified.
+func TestClassifyUnverifiedMarksFactlessTypeChanges(t *testing.T) {
+	verified, err := planner.Classify(
+		"ALTER TABLE t ALTER COLUMN v50 TYPE varchar(100)", facts)
+	require.NoError(t, err)
+	require.Len(t, verified.Decisions, 1)
+	assert.Equal(t, planner.RouteNative, verified.Decisions[0].Route)
+	assert.False(t, verified.Decisions[0].Unverified)
+
+	factless, err := planner.Classify(
+		"ALTER TABLE t ALTER COLUMN v50 TYPE varchar(100)", planner.Facts{})
+	require.NoError(t, err)
+	require.Len(t, factless.Decisions, 1)
+	assert.Equal(t, planner.RouteCopyAndSwap, factless.Decisions[0].Route)
+	assert.True(t, factless.Decisions[0].Unverified)
+
+	using, err := planner.Classify(
+		"ALTER TABLE t ALTER COLUMN txt TYPE jsonb USING txt::jsonb", planner.Facts{})
+	require.NoError(t, err)
+	require.Len(t, using.Decisions, 1)
+	assert.Equal(t, planner.RouteCopyAndSwap, using.Decisions[0].Route)
+	assert.False(t, using.Decisions[0].Unverified)
+}
+
 // TestClassifyReferenceRows is the golden mapping: one case per row of
 // docs/postgres-online-ddl-reference.md. saferSteps is the length of the
 // expected safer sequence (0 when the decision carries none).
diff --git a/pkg/statement/split.go b/pkg/statement/split.go
new file mode 100644
index 0000000..5592e97
--- /dev/null
+++ b/pkg/statement/split.go
@@ -0,0 +1,91 @@
+package statement
+
+import (
+	"fmt"
+	"strings"
+
+	pganalyze "github.com/pganalyze/pg_query_go/v6"
+	pgquery "github.com/wasilibs/go-pgquery"
+)
+
+// SourceStatement is one script statement located in its source: the
+// verbatim text plus the position of its first token, so a consumer can
+// point a finding back at the exact place in the file it came from.
+type SourceStatement struct {
+	// SQL is the statement's verbatim source text, without the trailing
+	// semicolon, so it can be found in the source by exact match.
+	SQL string
+	// Line is the 1-based source line of the statement's first token.
+	Line int
+	// Column is the 1-based source column of the statement's first token.
+	Column int
+}
+
+// Split parses a script with the PostgreSQL grammar and returns each
+// statement with its verbatim text and source position, in input order.
+// Every statement is also reprinted through the deparser as a validation
+// gate: a statement the grammar cannot roundtrip is an error, never a
+// guess. An empty script returns no statements; a parse failure anywhere
+// in the script is surfaced to the caller, never guessed around.
+func Split(sql string) ([]SourceStatement, error) {
+	tree, err := pgquery.Parse(sql)
+	if err != nil {
+		return nil, fmt.Errorf("parse script: %w", err)
+	}
+	scan, err := pgquery.Scan(sql)
+	if err != nil {
+		return nil, fmt.Errorf("scan script: %w", err)
+	}
+	stmts := make([]SourceStatement, 0, len(tree.GetStmts()))
+	for i, raw := range tree.GetStmts() {
+		if _, err := deparseOne(raw.GetStmt()); err != nil {
+			return nil, fmt.Errorf("statement %d: %w", i+1, err)
+		}
+		stmts = append(stmts, locate(sql, scan.GetTokens(), raw))
+	}
+	return stmts, nil
+}
+
+// locate slices one statement's verbatim text out of the script and
+// computes its position. The parser's statement range begins where the
+// previous statement ended, so the first non-comment token inside the
+// range — not the range start — is the statement's true beginning;
+// leading comments and whitespace stay out of the reported text.
+func locate(sql string, tokens []*pganalyze.ScanToken, raw *pganalyze.RawStmt) SourceStatement {
+	bound := int(raw.GetStmtLocation()) + int(raw.GetStmtLen())
+	// The parser marks the script's final statement with a zero length,
+	// meaning "through the end of the input".
+	if raw.GetStmtLen() == 0 {
+		bound = len(sql)
+	}
+	// The statement's reported text runs from its first code token to its
+	// last, so surrounding comments, whitespace, and the trailing
+	// semicolon stay out of it.
+	begin, end := int(raw.GetStmtLocation()), bound
+	first := false
+	for _, tok := range tokens {
+		if int(tok.GetStart()) < begin || int(tok.GetEnd()) > bound ||
+			isComment(tok) || tok.GetToken() == semicolonToken {
+			continue
+		}
+		if !first {
+			begin, first = int(tok.GetStart()), true
+		}
+		end = int(tok.GetEnd())
+	}
+	lastNewline := strings.LastIndexByte(sql[:begin], '\n')
+	return SourceStatement{
+		SQL:    sql[begin:end],
+		Line:   1 + strings.Count(sql[:begin], "\n"),
+		Column: begin - lastNewline,
+	}
+}
+
+// semicolonToken is the lexer token for the statement separator ";".
+const semicolonToken = pganalyze.Token_ASCII_59
+
+// isComment reports whether a lexer token is an SQL (--) or C-style
+// (/* */) comment.
+func isComment(tok *pganalyze.ScanToken) bool {
+	return tok.GetToken() == pganalyze.Token_SQL_COMMENT || tok.GetToken() == pganalyze.Token_C_COMMENT
+}
diff --git a/pkg/statement/split_test.go b/pkg/statement/split_test.go
new file mode 100644
index 0000000..2de0561
--- /dev/null
+++ b/pkg/statement/split_test.go
@@ -0,0 +1,57 @@
+package statement_test
+
+import (
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+	"github.com/stretchr/testify/require"
+
+	"github.com/block/pg-sprite/pkg/statement"
+)
+
+func TestSplitReturnsVerbatimStatementsWithPositions(t *testing.T) {
+	stmts, err := statement.Split(`-- a leading comment
+create table t (id int);
+ALTER TABLE t
+	ADD COLUMN c text;`)
+	require.NoError(t, err)
+	assert.Equal(t, []statement.SourceStatement{
+		{SQL: "create table t (id int)", Line: 2, Column: 1},
+		{SQL: "ALTER TABLE t\n\tADD COLUMN c text", Line: 3, Column: 1},
+	}, stmts)
+}
+
+// A statement's position is its first code token, not the start of the
+// parser's statement range — leading comments and whitespace between
+// statements stay out of the reported text and position.
+func TestSplitPositionSkipsLeadingComments(t *testing.T) {
+	stmts, err := statement.Split(
+		"CREATE TABLE ok (id int);\n\n-- why we drop it\n/* twice */ DROP TABLE old;")
+	require.NoError(t, err)
+	require.Len(t, stmts, 2)
+	assert.Equal(t, statement.SourceStatement{
+		SQL: "DROP TABLE old", Line: 4, Column: 13,
+	}, stmts[1])
+}
+
+// The script's final statement carries no length in the parse tree; its
+// text still ends at its last code token, not at the end of the input.
+func TestSplitFinalStatementExcludesTrailingNoise(t *testing.T) {
+	stmts, err := statement.Split("DROP TABLE old ; -- gone")
+	require.NoError(t, err)
+	require.Len(t, stmts, 1)
+	assert.Equal(t, statement.SourceStatement{
+		SQL: "DROP TABLE old", Line: 1, Column: 1,
+	}, stmts[0])
+}
+
+func TestSplitEmptyScriptReturnsNoStatements(t *testing.T) {
+	stmts, err := statement.Split("  \n\t")
+	require.NoError(t, err)
+	assert.Empty(t, stmts)
+}
+
+func TestSplitParseFailureIsError(t *testing.T) {
+	_, err := statement.Split("CREATE TABLE t (id int); CREATE TABEL u (id int)")
+	require.Error(t, err)
+}