diff --git a/.gitignore b/.gitignore
index 2850867..59da4ce 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,6 @@
 # Local-only running-state file (current state, decisions in flight, next
 # steps). Never committed; see CLAUDE.md.
 /HANDOFF.md
+
+# Agent worktrees (created by subagent isolation; never commit)
+/.claude/worktrees/
diff --git a/docs/06-schema-reference.md b/docs/06-schema-reference.md
index f831a26..7817a11 100644
--- a/docs/06-schema-reference.md
+++ b/docs/06-schema-reference.md
@@ -93,6 +93,7 @@ Each key under `entities` is the entity's canonical name (PascalCase, e.g.
 | Field | Type | Required | Notes |
 |---|---|---|---|
 | `definition` | string | yes | Two to four sentences: what it is, what it is not. |
+| `subtypeOf` | string | no | Names the entity this one is a kind of (an is-a link). Must reference a defined entity. |
 | `relationships` | list | no | See [Relationship](#relationship). |
 | `attributes` | list | no | See [Attribute](#attribute). |
 | `actions` | list | no | Mutations the system exposes. See [Action](#action). |
@@ -111,6 +112,16 @@ derived entities — per-entity styling is unverified across the Mermaid
 versions in play, so the ER stays a deliberately lossy view; the Markdown text
 is the source of truth.
 
+Use `subtypeOf` for generalization — when one entity *is a kind of* another
+(a `Card` is a `PaymentMethod`). The child declares it, and it must name a
+defined entity; the linter errors on an undefined parent or a cycle. A parent's
+invariants are understood to cover its subtypes, so a subtype that adds no rule
+of its own is not flagged for having no invariants. The Mermaid ER diagram does
+not draw the is-a link — erDiagram has no generalization notation, so the
+hierarchy lives in the rendered Markdown (each child names its supertype and
+each parent lists its subtypes), a deliberately lossy ER per the same principle
+as derived entities.
+
 ## Relationship
 
 | Field | Type | Required | Notes |
diff --git a/internal/lint/lint.go b/internal/lint/lint.go
index ec31571..2142136 100644
--- a/internal/lint/lint.go
+++ b/internal/lint/lint.go
@@ -105,6 +105,7 @@ func Run(data []byte) (*Result, error) {
 
 	runSemantic(m, res)
 	runRelationshipShape(m, res)
+	runSubtypes(m, res)
 	runReciprocity(m, res)
 	runCompleteness(m, res)
 
@@ -504,6 +505,73 @@ func sideInverted(s string) bool {
 	return err1 == nil && err2 == nil && min > max
 }
 
+// runSubtypes validates the is-a links: a subtypeOf must name a defined entity,
+// and the chain of subtypeOf links must not cycle (an entity cannot be a kind
+// of itself, directly or transitively).
+func runSubtypes(m *model.Model, res *Result) {
+	for _, name := range m.EntityNames() {
+		parent := m.Entities[name].SubtypeOf
+		if parent == "" {
+			continue
+		}
+		if _, ok := m.Entities[parent]; !ok {
+			res.Findings = append(res.Findings, Finding{
+				Severity: SeverityError,
+				Category: CategorySemantic,
+				Path:     fmt.Sprintf("/entities/%s/subtypeOf", name),
+				Message:  fmt.Sprintf("entity %q is a subtype of undefined entity %q", name, parent),
+			})
+			continue
+		}
+		if subtypeChainCycles(m, name) {
+			res.Findings = append(res.Findings, Finding{
+				Severity: SeverityError,
+				Category: CategorySemantic,
+				Path:     fmt.Sprintf("/entities/%s/subtypeOf", name),
+				Message:  fmt.Sprintf("entity %q has a cyclic subtypeOf chain: an entity cannot be a kind of itself, directly or transitively", name),
+			})
+		}
+	}
+}
+
+// subtypeChainCycles reports whether following name's subtypeOf links revisits
+// an entity, which means name is (transitively) a subtype of itself. It stops
+// at an undefined parent, which is reported separately.
+func subtypeChainCycles(m *model.Model, name string) bool {
+	seen := map[string]bool{}
+	for cur := name; cur != ""; {
+		e, ok := m.Entities[cur]
+		if !ok {
+			return false
+		}
+		if seen[cur] {
+			return true
+		}
+		seen[cur] = true
+		cur = e.SubtypeOf
+	}
+	return false
+}
+
+// inheritsInvariants reports whether any ancestor of name (via subtypeOf) has an
+// invariant, so a subtype's own empty invariant list is covered by its parent.
+// The walk is cycle-safe and stops at an undefined parent.
+func inheritsInvariants(m *model.Model, name string) bool {
+	seen := map[string]bool{name: true}
+	for cur := m.Entities[name].SubtypeOf; cur != "" && !seen[cur]; {
+		e, ok := m.Entities[cur]
+		if !ok {
+			return false
+		}
+		if len(e.Invariants) > 0 {
+			return true
+		}
+		seen[cur] = true
+		cur = e.SubtypeOf
+	}
+	return false
+}
+
 // runReciprocity checks that a relationship declared from both sides agrees:
 // B→A must declare the inverse of A→B's cardinality. A contradiction (e.g. A
 // says "1:n" B while B says "1:1" A) is an error — the model can't be both, and
@@ -576,9 +644,9 @@ func runReciprocity(m *model.Model, res *Result) {
 }
 
 func runCompleteness(m *model.Model, res *Result) {
-	// Entities with no invariants.
+	// Entities with no invariants — unless a supertype's invariants cover them.
 	for _, name := range m.EntityNames() {
-		if len(m.Entities[name].Invariants) == 0 {
+		if len(m.Entities[name].Invariants) == 0 && !inheritsInvariants(m, name) {
 			res.Findings = append(res.Findings, Finding{
 				Severity: SeverityWarning,
 				Category: CategoryCompleteness,
diff --git a/internal/lint/lint_test.go b/internal/lint/lint_test.go
index eaf02e1..3a25ca6 100644
--- a/internal/lint/lint_test.go
+++ b/internal/lint/lint_test.go
@@ -970,3 +970,93 @@ entities:
 		t.Fatalf("should not also emit the symmetric-misuse error: %+v", res.Findings)
 	}
 }
+
+// TestADR_0004_UndefinedSupertype pins that a subtypeOf naming no defined
+// entity is a semantic error.
+func TestADR_0004_UndefinedSupertype(t *testing.T) {
+	src := `
+kind: DomainModel
+version: v1
+entities:
+  Card:
+    definition: A card that claims to be a kind of an undefined thing.
+    subtypeOf: PaymentMethod
+`
+	res, err := Run([]byte(src))
+	if err != nil {
+		t.Fatal(err)
+	}
+	if !findingWithMessage(res.Findings, "subtype of undefined entity") {
+		t.Fatalf("expected an undefined-supertype error, got: %+v", res.Findings)
+	}
+}
+
+// TestADR_0004_SubtypeInheritsInvariants pins that a supertype's invariants
+// cover a subtype for completeness: a subtype with no invariants of its own is
+// not flagged when its parent has them, while an unrelated empty entity is.
+func TestADR_0004_SubtypeInheritsInvariants(t *testing.T) {
+	src := `
+kind: DomainModel
+version: v1
+entities:
+  PaymentMethod:
+    definition: A way to pay.
+    invariants:
+      - id: pm-usable
+        statement: A `+"`PaymentMethod`"+` is either active or revoked.
+  Card:
+    definition: A payment method backed by a card; adds no rule of its own.
+    subtypeOf: PaymentMethod
+  Cash:
+    definition: A standalone entity with no rule and no parent.
+`
+	res, err := Run([]byte(src))
+	if err != nil {
+		t.Fatal(err)
+	}
+	if findingWithMessage(res.Findings, `"Card" has no invariants`) {
+		t.Fatalf("subtype should inherit its parent's invariants for completeness: %+v", res.Findings)
+	}
+	if !findingWithMessage(res.Findings, `"Cash" has no invariants`) {
+		t.Fatalf("an unrelated empty entity should still be flagged: %+v", res.Findings)
+	}
+}
+
+// TestSubtypeCycleDetected pins that a self- or mutually-cyclic subtypeOf chain
+// is a semantic error rather than an infinite walk.
+func TestSubtypeCycleDetected(t *testing.T) {
+	self := `
+kind: DomainModel
+version: v1
+entities:
+  A:
+    definition: An entity that is a kind of itself.
+    subtypeOf: A
+`
+	res, err := Run([]byte(self))
+	if err != nil {
+		t.Fatal(err)
+	}
+	if !findingWithMessage(res.Findings, "cyclic subtypeOf chain") {
+		t.Fatalf("expected a self-cycle error, got: %+v", res.Findings)
+	}
+
+	mutual := `
+kind: DomainModel
+version: v1
+entities:
+  Alpha:
+    definition: A kind of Beta.
+    subtypeOf: Beta
+  Beta:
+    definition: A kind of Alpha.
+    subtypeOf: Alpha
+`
+	res, err = Run([]byte(mutual))
+	if err != nil {
+		t.Fatal(err)
+	}
+	if !findingWithMessage(res.Findings, "cyclic subtypeOf chain") {
+		t.Fatalf("expected a mutual-cycle error, got: %+v", res.Findings)
+	}
+}
diff --git a/internal/model/model.go b/internal/model/model.go
index 9c59774..9c1e925 100644
--- a/internal/model/model.go
+++ b/internal/model/model.go
@@ -49,7 +49,10 @@ type EnumValue struct {
 
 // Entity is a named concept in the domain.
 type Entity struct {
-	Definition    string         `json:"definition"`
+	Definition string `json:"definition"`
+	// SubtypeOf names the entity this one is a kind of (an is-a link). The
+	// parent's invariants are understood to cover this entity too.
+	SubtypeOf     string         `json:"subtypeOf,omitempty"`
 	Relationships []Relationship `json:"relationships,omitempty"`
 	Attributes    []Attribute    `json:"attributes,omitempty"`
 	Actions       []Action       `json:"actions,omitempty"`
diff --git a/internal/render/markdown/markdown.go b/internal/render/markdown/markdown.go
index 79555cf..e9f963c 100644
--- a/internal/render/markdown/markdown.go
+++ b/internal/render/markdown/markdown.go
@@ -107,6 +107,14 @@ func renderEntities(b *strings.Builder, m *model.Model) {
 	if len(names) == 0 {
 		return
 	}
+	// Index subtypes by parent so each parent can list its kinds. names is
+	// sorted, so each child list is deterministic.
+	subtypes := map[string][]string{}
+	for _, n := range names {
+		if p := m.Entities[n].SubtypeOf; p != "" {
+			subtypes[p] = append(subtypes[p], n)
+		}
+	}
 	b.WriteString("## Entities\n\n")
 	for _, name := range names {
 		ent := m.Entities[name]
@@ -117,6 +125,17 @@ func renderEntities(b *strings.Builder, m *model.Model) {
 			b.WriteString("\n\n")
 		}
 
+		if ent.SubtypeOf != "" {
+			fmt.Fprintf(b, "**Subtype of** `%s`\n\n", ent.SubtypeOf)
+		}
+		if kids := subtypes[name]; len(kids) > 0 {
+			quoted := make([]string, len(kids))
+			for i, k := range kids {
+				quoted[i] = "`" + k + "`"
+			}
+			fmt.Fprintf(b, "**Subtypes** — %s\n\n", strings.Join(quoted, ", "))
+		}
+
 		if ent.Derived {
 			d := "**Derived.** Computed on demand from other state; never persisted."
 			if derivation := strings.TrimSpace(ent.Derivation); derivation != "" {
diff --git a/internal/render/markdown/markdown_test.go b/internal/render/markdown/markdown_test.go
index fdf6172..d7f2364 100644
--- a/internal/render/markdown/markdown_test.go
+++ b/internal/render/markdown/markdown_test.go
@@ -131,3 +131,21 @@ func TestGoldenExample(t *testing.T) {
 			golden, src, firstDiff(string(want), got))
 	}
 }
+
+// TestRenderEntity_SubtypeHierarchy checks that a child names its supertype and
+// a parent lists its subtypes.
+func TestRenderEntity_SubtypeHierarchy(t *testing.T) {
+	m := &model.Model{Entities: map[string]model.Entity{
+		"PaymentMethod": {Definition: "A way to pay."},
+		"Card":          {Definition: "A card.", SubtypeOf: "PaymentMethod"},
+		"BankTransfer":  {Definition: "A transfer.", SubtypeOf: "PaymentMethod"},
+	}}
+	got := Render(m)
+	if !strings.Contains(got, "**Subtype of** `PaymentMethod`") {
+		t.Errorf("expected child to name its supertype:\n%s", got)
+	}
+	// names render alphabetically, so BankTransfer precedes Card.
+	if !strings.Contains(got, "**Subtypes** — `BankTransfer`, `Card`") {
+		t.Errorf("expected parent to list its subtypes:\n%s", got)
+	}
+}
diff --git a/internal/schema/v1/modelith.schema.json b/internal/schema/v1/modelith.schema.json
index 6c07dfe..dae7599 100644
--- a/internal/schema/v1/modelith.schema.json
+++ b/internal/schema/v1/modelith.schema.json
@@ -109,6 +109,11 @@
           "type": "string",
           "minLength": 1
         },
+        "subtypeOf": {
+          "description": "Names the entity this one is a kind of — an is-a / generalization link. Must reference a defined entity. The parent's invariants are understood to hold for this entity too.",
+          "type": "string",
+          "pattern": "^[A-Z][A-Za-z0-9]+$"
+        },
         "relationships": {
           "description": "How this entity relates to others. A relationship is declared under one entity and names a target; it may be declared from either end (the linter checks that the two views agree). When one entity is intuitively the parent — it owns or contains the other, or is the \"one\" side of a one-to-many — prefer declaring the relationship there.",
           "type": "array",