diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7f391449f3..829fa35112 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Use `testcontainers` instead of `ory/dockertest` for running containers in integration tests (https://github.com/authzed/spicedb/pull/2782)
 
 ### Fixed
+- Query Planner: recursive relations (e.g. `member: user | group#member`) no longer report a subject as only conditionally reachable when an uncaveated path makes it unconditional, and a traversal that exceeds the maximum recursion depth now returns an error instead of a silently truncated result (experimental `--experimental-query-plan`) (https://github.com/authzed/spicedb/pull/3220)
 - Fixed a nil pointer dereference panic in `CheckBulkPermissions` that could occur under concurrent load when a tracing-enabled check shared a singleflight dispatch with a non-tracing bulk check. Debug-enabled checks are no longer singleflighted together with non-debug checks. (https://github.com/authzed/spicedb/pull/3174)
 - CockroachDB: deletes performed by CockroachDB's row-level TTL job for expired relationships are no longer emitted as `DELETE` events by the Watch API. On CockroachDB ≥ 24.1, SpiceDB sets the `ttl_disable_changefeed_replication` storage parameter on the relationship tables at startup (if it lacks `ALTER TABLE` privileges, it logs a warning with the statement to run manually); on older versions a startup warning is logged and TTL deletes continue to be emitted. Note that the parameter affects any changefeed over these tables — external changefeeds that want TTL deletes can opt back in with `ignore_disable_changefeed_replication`. Delete-only transactions also no longer write an internal transaction-metadata marker row, reducing write amplification. (https://github.com/authzed/spicedb/pull/3210)
 - When SpiceDB loses a connection to a CockroachDB node, every read happening in the server blocks for a short period of time (https://github.com/authzed/spicedb/pull/3181)
diff --git a/internal/caveats/canonical.go b/internal/caveats/canonical.go
new file mode 100644
index 0000000000..0cd0ff9b74
--- /dev/null
+++ b/internal/caveats/canonical.go
@@ -0,0 +1,309 @@
+package caveats
+
+import (
+	"sort"
+	"strings"
+
+	"google.golang.org/protobuf/proto"
+
+	pkgcaveats "github.com/authzed/spicedb/pkg/caveats"
+	core "github.com/authzed/spicedb/pkg/proto/core/v1"
+)
+
+// Condition is a canonical, order-independent representation of a caveat
+// expression as a disjunctive normal form (DNF): an OR of conjuncts, where each
+// conjunct is an AND of atoms. It exists so that recursive traversals can decide
+// whether a newly-discovered path *weakens* the condition under which an object
+// is reachable — the termination guarantee of the semi-naive fixpoint.
+//
+// Two properties make that guarantee hold:
+//   - AND is idempotent and commutative: c1 ∧ c2 ∧ c1 collapses to {c1, c2}, so
+//     the set of distinct conjuncts is finite.
+//   - ⊤ (unconditional) is absorbing under OR: once an object is reachable
+//     unconditionally, no further path can weaken it.
+//
+// The zero value is the "false" condition (no disjuncts); use Top() for the
+// unconditional condition and FromExpression to derive one from a caveat.
+type Condition struct {
+	top       bool
+	disjuncts [][]atom // OR of conjuncts; each conjunct sorted+deduped by atom key, non-empty
+}
+
+// atom is a single indivisible leaf of a condition: a contextualized caveat, or
+// an opaque (e.g. negated) subexpression. key is the canonical identity used for
+// dedup, sorting and comparison; expr is retained so the original expression can
+// be rebuilt, since the key alone cannot recover a caveat's context.
+type atom struct {
+	key  string
+	expr *core.CaveatExpression
+}
+
+// Top returns the unconditional (always-true) condition.
+func Top() Condition {
+	return Condition{top: true}
+}
+
+// FromExpression converts a caveat expression into its canonical DNF. A nil
+// expression is unconditional and yields Top().
+func FromExpression(expr *core.CaveatExpression) Condition {
+	if expr == nil {
+		return Top()
+	}
+	return fromExpr(expr)
+}
+
+func fromExpr(expr *core.CaveatExpression) Condition {
+	if leaf := expr.GetCaveat(); leaf != nil {
+		return singleAtom(atom{key: caveatAtomKey(leaf), expr: expr})
+	}
+
+	op := expr.GetOperation()
+	if op == nil {
+		return singleAtom(atom{key: opaqueAtomKey(expr), expr: expr})
+	}
+
+	switch op.GetOp() {
+	case core.CaveatOperation_AND:
+		result := Top()
+		for _, child := range op.GetChildren() {
+			result = result.And(fromExpr(child))
+		}
+		return result
+
+	case core.CaveatOperation_OR:
+		var result Condition // the zero value is the "false" condition
+		for _, child := range op.GetChildren() {
+			result, _ = result.Or(fromExpr(child))
+		}
+		return result
+
+	default:
+		// NOT (and anything unrecognized) is treated as an opaque atom: we do not
+		// distribute negation, which keeps the atom set finite and the result sound
+		// (conservative — it may report "changed" when logically unchanged).
+		return singleAtom(atom{key: opaqueAtomKey(expr), expr: expr})
+	}
+}
+
+// IsTop reports whether the condition is unconditional.
+func (c Condition) IsTop() bool {
+	return c.top
+}
+
+// Disjuncts returns the number of DNF disjuncts (0 for Top or false).
+func (c Condition) Disjuncts() int {
+	return len(c.disjuncts)
+}
+
+// And returns the canonical conjunction of the two conditions.
+func (c Condition) And(other Condition) Condition {
+	if c.top {
+		return other
+	}
+	if other.top {
+		return c
+	}
+	// false AND x == false
+	if len(c.disjuncts) == 0 || len(other.disjuncts) == 0 {
+		return Condition{}
+	}
+
+	// Distribute: (A1 ∨ A2) ∧ (B1 ∨ B2) == (A1∧B1) ∨ (A1∧B2) ∨ (A2∧B1) ∨ (A2∧B2).
+	product := make([][]atom, 0, len(c.disjuncts)*len(other.disjuncts))
+	for _, a := range c.disjuncts {
+		for _, b := range other.disjuncts {
+			combined := make([]atom, 0, len(a)+len(b))
+			combined = append(combined, a...)
+			combined = append(combined, b...)
+			product = append(product, combined)
+		}
+	}
+	return normalizeCondition(product)
+}
+
+// Or returns the canonical disjunction of the two conditions, and reports whether
+// the result differs from the receiver — i.e. whether other *weakened* c.
+func (c Condition) Or(other Condition) (Condition, bool) {
+	if c.top {
+		return c, false
+	}
+	if other.top {
+		return Top(), true
+	}
+
+	combined := make([][]atom, 0, len(c.disjuncts)+len(other.disjuncts))
+	combined = append(combined, c.disjuncts...)
+	combined = append(combined, other.disjuncts...)
+	result := normalizeCondition(combined)
+	return result, !result.equalTo(c)
+}
+
+// Expression rebuilds a caveat expression equivalent to this condition. Top()
+// (and the degenerate false condition) yield nil.
+func (c Condition) Expression() *core.CaveatExpression {
+	if c.top || len(c.disjuncts) == 0 {
+		return nil
+	}
+
+	var result *core.CaveatExpression
+	for _, conjunct := range c.disjuncts {
+		var conj *core.CaveatExpression
+		for _, a := range conjunct {
+			conj = And(conj, a.expr)
+		}
+		result = Or(result, conj)
+	}
+	return result
+}
+
+// String returns a deterministic, human-readable rendering of the DNF.
+func (c Condition) String() string {
+	if c.top {
+		return "true"
+	}
+	if len(c.disjuncts) == 0 {
+		return "false"
+	}
+	parts := make([]string, len(c.disjuncts))
+	for i, conjunct := range c.disjuncts {
+		keys := make([]string, len(conjunct))
+		for j, a := range conjunct {
+			keys[j] = a.key
+		}
+		parts[i] = strings.Join(keys, " & ")
+	}
+	return strings.Join(parts, " | ")
+}
+
+func (c Condition) equalTo(other Condition) bool {
+	if c.top != other.top || len(c.disjuncts) != len(other.disjuncts) {
+		return false
+	}
+	for i := range c.disjuncts {
+		if len(c.disjuncts[i]) != len(other.disjuncts[i]) {
+			return false
+		}
+		for j := range c.disjuncts[i] {
+			if c.disjuncts[i][j].key != other.disjuncts[i][j].key {
+				return false
+			}
+		}
+	}
+	return true
+}
+
+func singleAtom(a atom) Condition {
+	return normalizeCondition([][]atom{{a}})
+}
+
+// normalizeCondition sorts and dedupes atoms within each conjunct, drops any
+// conjunct subsumed by a smaller one, dedupes identical conjuncts, and sorts the
+// disjuncts — yielding the canonical form. An empty conjunct means "true" and
+// collapses the whole condition to Top.
+func normalizeCondition(disjuncts [][]atom) Condition {
+	reduced := make([][]atom, 0, len(disjuncts))
+	for _, conjunct := range disjuncts {
+		conjunct = sortDedupeAtoms(conjunct)
+		if len(conjunct) == 0 {
+			return Top()
+		}
+		reduced = append(reduced, conjunct)
+	}
+
+	reduced = subsumeAndDedupe(reduced)
+	sort.Slice(reduced, func(i, j int) bool {
+		return conjunctKey(reduced[i]) < conjunctKey(reduced[j])
+	})
+	return Condition{disjuncts: reduced}
+}
+
+func sortDedupeAtoms(atoms []atom) []atom {
+	if len(atoms) <= 1 {
+		return atoms
+	}
+	cp := make([]atom, len(atoms))
+	copy(cp, atoms)
+	sort.Slice(cp, func(i, j int) bool { return cp[i].key < cp[j].key })
+
+	out := cp[:1]
+	for _, a := range cp[1:] {
+		if a.key != out[len(out)-1].key {
+			out = append(out, a)
+		}
+	}
+	return out
+}
+
+// subsumeAndDedupe removes duplicate conjuncts and any conjunct that is a strict
+// superset of another (a superset is a stronger, redundant constraint in an OR).
+func subsumeAndDedupe(disjuncts [][]atom) [][]atom {
+	seen := make(map[string]bool, len(disjuncts))
+	unique := make([][]atom, 0, len(disjuncts))
+	for _, conjunct := range disjuncts {
+		key := conjunctKey(conjunct)
+		if !seen[key] {
+			seen[key] = true
+			unique = append(unique, conjunct)
+		}
+	}
+
+	keep := make([][]atom, 0, len(unique))
+	for i, a := range unique {
+		subsumed := false
+		for j, b := range unique {
+			if i != j && len(b) < len(a) && isAtomSubset(b, a) {
+				subsumed = true
+				break
+			}
+		}
+		if !subsumed {
+			keep = append(keep, a)
+		}
+	}
+	return keep
+}
+
+// isAtomSubset reports whether every atom in b (sorted by key) appears in a
+// (sorted by key).
+func isAtomSubset(b, a []atom) bool {
+	i := 0
+	for _, x := range b {
+		for i < len(a) && a[i].key < x.key {
+			i++
+		}
+		if i >= len(a) || a[i].key != x.key {
+			return false
+		}
+		i++
+	}
+	return true
+}
+
+func conjunctKey(conjunct []atom) string {
+	keys := make([]string, len(conjunct))
+	for i, a := range conjunct {
+		keys[i] = a.key
+	}
+	return strings.Join(keys, "\x00")
+}
+
+func caveatAtomKey(c *core.ContextualizedCaveat) string {
+	name := c.GetCaveatName()
+	ctx := c.GetContext()
+	if ctx == nil || len(ctx.GetFields()) == 0 {
+		return name
+	}
+	stable, err := pkgcaveats.StableContextStringForHashing(ctx)
+	if err != nil {
+		return name + "@" + ctx.String()
+	}
+	return name + "@" + stable
+}
+
+func opaqueAtomKey(expr *core.CaveatExpression) string {
+	encoded, err := proto.MarshalOptions{Deterministic: true}.Marshal(expr)
+	if err != nil {
+		return "opaque:" + expr.String()
+	}
+	return "opaque:" + string(encoded)
+}
diff --git a/internal/caveats/canonical_test.go b/internal/caveats/canonical_test.go
new file mode 100644
index 0000000000..e74beddcef
--- /dev/null
+++ b/internal/caveats/canonical_test.go
@@ -0,0 +1,109 @@
+package caveats
+
+import (
+	"testing"
+
+	"github.com/stretchr/testify/require"
+)
+
+func TestConditionTop(t *testing.T) {
+	require.True(t, Top().IsTop())
+	require.Equal(t, "true", Top().String())
+
+	// A nil expression is unconditional.
+	require.True(t, FromExpression(nil).IsTop())
+
+	// A single caveat is conditional.
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+	require.False(t, c1.IsTop())
+	require.Equal(t, "cav1", c1.String())
+	require.Equal(t, 1, c1.Disjuncts())
+}
+
+func TestConditionAndIsIdempotent(t *testing.T) {
+	// c1 ∧ c2 ∧ c1 must collapse to the two-atom conjunct {c1, c2}.
+	expr := And(And(CaveatExprForTesting("cav1"), CaveatExprForTesting("cav2")), CaveatExprForTesting("cav1"))
+	c := FromExpression(expr)
+	require.Equal(t, "cav1 & cav2", c.String())
+	require.Equal(t, 1, c.Disjuncts())
+}
+
+func TestConditionAndIsCommutative(t *testing.T) {
+	a := FromExpression(And(CaveatExprForTesting("cav1"), CaveatExprForTesting("cav2")))
+	b := FromExpression(And(CaveatExprForTesting("cav2"), CaveatExprForTesting("cav1")))
+	require.Equal(t, a.String(), b.String())
+}
+
+func TestConditionAndWithTopIsIdentity(t *testing.T) {
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+	require.Equal(t, "cav1", Top().And(c1).String())
+	require.Equal(t, "cav1", c1.And(Top()).String())
+}
+
+func TestConditionAndDistributesOverOr(t *testing.T) {
+	// (cav1 | cav2) & cav3 == (cav1 & cav3) | (cav2 & cav3)
+	expr := And(Or(CaveatExprForTesting("cav1"), CaveatExprForTesting("cav2")), CaveatExprForTesting("cav3"))
+	require.Equal(t, "cav1 & cav3 | cav2 & cav3", FromExpression(expr).String())
+}
+
+func TestConditionOrUnions(t *testing.T) {
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+	c2 := FromExpression(CaveatExprForTesting("cav2"))
+	res, changed := c1.Or(c2)
+	require.True(t, changed)
+	require.Equal(t, "cav1 | cav2", res.String())
+}
+
+func TestConditionOrIdempotentReportsUnchanged(t *testing.T) {
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+	res, changed := c1.Or(FromExpression(CaveatExprForTesting("cav1")))
+	require.False(t, changed, "OR-ing an identical condition must not report a change")
+	require.Equal(t, "cav1", res.String())
+}
+
+func TestConditionOrAbsorbsTop(t *testing.T) {
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+
+	// A conditional weakened by Top becomes unconditional (a change).
+	res, changed := c1.Or(Top())
+	require.True(t, res.IsTop())
+	require.True(t, changed)
+
+	// Top OR anything stays Top (no change).
+	res2, changed2 := Top().Or(c1)
+	require.True(t, res2.IsTop())
+	require.False(t, changed2)
+}
+
+func TestConditionOrSubsumesSuperset(t *testing.T) {
+	// cav1 ∨ (cav1 ∧ cav2): the two-atom conjunct is redundant (implies cav1), so
+	// the result is just cav1.
+	c1 := FromExpression(CaveatExprForTesting("cav1"))
+	c1and2 := FromExpression(And(CaveatExprForTesting("cav1"), CaveatExprForTesting("cav2")))
+
+	res, changed := c1.Or(c1and2)
+	require.Equal(t, "cav1", res.String())
+	require.False(t, changed, "adding a subsumed conjunct does not weaken the condition")
+
+	// The other direction: starting from the superset and adding cav1 weakens it.
+	res2, changed2 := c1and2.Or(c1)
+	require.Equal(t, "cav1", res2.String())
+	require.True(t, changed2)
+}
+
+func TestConditionContextDistinguishesAtoms(t *testing.T) {
+	// Same caveat name, different context => distinct atoms.
+	a := FromExpression(MustCaveatExprForTestingWithContext("cav1", map[string]any{"x": 1}))
+	b := FromExpression(MustCaveatExprForTestingWithContext("cav1", map[string]any{"x": 2}))
+	res, changed := a.Or(b)
+	require.True(t, changed)
+	require.Equal(t, 2, res.Disjuncts(), "different context must not be deduped")
+}
+
+func TestConditionExpressionRoundTrip(t *testing.T) {
+	require.Nil(t, Top().Expression())
+
+	orig := FromExpression(And(CaveatExprForTesting("cav1"), CaveatExprForTesting("cav2")))
+	rebuilt := FromExpression(orig.Expression())
+	require.Equal(t, orig.String(), rebuilt.String())
+}
diff --git a/internal/datastore/proxy/indexcheck/queryshapevalidators.go b/internal/datastore/proxy/indexcheck/queryshapevalidators.go
index d4afee48ce..935b6d260e 100644
--- a/internal/datastore/proxy/indexcheck/queryshapevalidators.go
+++ b/internal/datastore/proxy/indexcheck/queryshapevalidators.go
@@ -287,6 +287,38 @@ func validateQueryShape(queryShape queryshape.Shape, filter datastore.Relationsh
 		}
 		return nil
 
+	case queryshape.MatchingResourcesForSubject:
+		// The forward form of this shape, as issued by pkg/query/reader.go's
+		// QueryResources: the resource type and relation are pinned, the resource
+		// ID is never specified, and exactly one subject selector fully specifies
+		// the subject type and ID. The subject relation is possibly-specified, so
+		// it is intentionally not validated (mirroring the reverse validator).
+		if err := validateCaveatFilter(filter, queryShape); err != nil {
+			return err
+		}
+		if err := validateResourceType(filter.OptionalResourceType, queryShape, true); err != nil {
+			return err
+		}
+		if err := validateResourceIDs(filter.OptionalResourceIds, queryShape, false); err != nil {
+			return err
+		}
+		if err := validateResourceRelation(filter.OptionalResourceRelation, queryShape, true); err != nil {
+			return err
+		}
+		if err := validateSubjectsSelectors(filter.OptionalSubjectsSelectors, queryShape, true); err != nil {
+			return err
+		}
+		if len(filter.OptionalSubjectsSelectors) != 1 {
+			return fmt.Errorf("exactly one subjects selector required for %s", queryShape)
+		}
+		if err := validateSubjectType(filter.OptionalSubjectsSelectors[0].OptionalSubjectType, queryShape); err != nil {
+			return err
+		}
+		if err := validateSubjectIDs(filter.OptionalSubjectsSelectors[0].OptionalSubjectIds, queryShape, true); err != nil {
+			return err
+		}
+		return nil
+
 	case queryshape.Varying:
 		// Nothing to validate.
 		return nil
diff --git a/internal/datastore/proxy/indexcheck/queryshapevalidators_test.go b/internal/datastore/proxy/indexcheck/queryshapevalidators_test.go
index 0c081aa269..6c6845d2f0 100644
--- a/internal/datastore/proxy/indexcheck/queryshapevalidators_test.go
+++ b/internal/datastore/proxy/indexcheck/queryshapevalidators_test.go
@@ -738,6 +738,88 @@ func TestValidateQueryShape(t *testing.T) {
 			expectError: true,
 			errorMsg:    "subject relation required",
 		},
+		{
+			// The exact filter pkg/query/reader.go QueryResources builds for a
+			// forward MatchingResourcesForSubject query, with an ellipsis subject.
+			name:  "MatchingResourcesForSubject - valid, ellipsis subject",
+			shape: queryshape.MatchingResourcesForSubject,
+			filter: datastore.RelationshipsFilter{
+				OptionalResourceType:     "document",
+				OptionalResourceRelation: "viewer",
+				OptionalSubjectsSelectors: []datastore.SubjectsSelector{
+					{
+						OptionalSubjectType: "user",
+						OptionalSubjectIds:  []string{"user1"},
+					},
+				},
+			},
+			expectError: false,
+		},
+		{
+			// subject_relation is possibly-specified (🅿️) for this shape, so a
+			// non-ellipsis subject relation must also be accepted.
+			name:  "MatchingResourcesForSubject - valid, non-ellipsis subject relation",
+			shape: queryshape.MatchingResourcesForSubject,
+			filter: datastore.RelationshipsFilter{
+				OptionalResourceType:     "document",
+				OptionalResourceRelation: "viewer",
+				OptionalSubjectsSelectors: []datastore.SubjectsSelector{
+					{
+						OptionalSubjectType: "group",
+						OptionalSubjectIds:  []string{"admins"},
+						RelationFilter:      datastore.SubjectRelationFilter{}.WithNonEllipsisRelation("member"),
+					},
+				},
+			},
+			expectError: false,
+		},
+		{
+			name:  "MatchingResourcesForSubject - missing resource type",
+			shape: queryshape.MatchingResourcesForSubject,
+			filter: datastore.RelationshipsFilter{
+				OptionalResourceRelation: "viewer",
+				OptionalSubjectsSelectors: []datastore.SubjectsSelector{
+					{
+						OptionalSubjectType: "user",
+						OptionalSubjectIds:  []string{"user1"},
+					},
+				},
+			},
+			expectError: true,
+			errorMsg:    "resource type required",
+		},
+		{
+			name:  "MatchingResourcesForSubject - has resource ids",
+			shape: queryshape.MatchingResourcesForSubject,
+			filter: datastore.RelationshipsFilter{
+				OptionalResourceType:     "document",
+				OptionalResourceIds:      []string{"doc1"},
+				OptionalResourceRelation: "viewer",
+				OptionalSubjectsSelectors: []datastore.SubjectsSelector{
+					{
+						OptionalSubjectType: "user",
+						OptionalSubjectIds:  []string{"user1"},
+					},
+				},
+			},
+			expectError: true,
+			errorMsg:    "no optional resource ids allowed",
+		},
+		{
+			name:  "MatchingResourcesForSubject - missing subject ids",
+			shape: queryshape.MatchingResourcesForSubject,
+			filter: datastore.RelationshipsFilter{
+				OptionalResourceType:     "document",
+				OptionalResourceRelation: "viewer",
+				OptionalSubjectsSelectors: []datastore.SubjectsSelector{
+					{
+						OptionalSubjectType: "user",
+					},
+				},
+			},
+			expectError: true,
+			errorMsg:    "subject ids required",
+		},
 		{
 			name:        "Unknown shape - error",
 			shape:       "unknown-shape",
diff --git a/internal/services/integrationtesting/queryconsistency/query_plan_consistency_test.go b/internal/services/integrationtesting/queryconsistency/query_plan_consistency_test.go
index 24b11b6273..cfd2fcbd06 100644
--- a/internal/services/integrationtesting/queryconsistency/query_plan_consistency_test.go
+++ b/internal/services/integrationtesting/queryconsistency/query_plan_consistency_test.go
@@ -81,24 +81,23 @@ func runQueryPlanConsistencyForFile(t *testing.T, filePath string) {
 	runQueryPlanAssertions(t, handle)
 
 	t.Run("lookup_resources", func(t *testing.T) {
-		if os.Getenv("TEST_QUERY_PLAN_RESOURCES") == "" {
-			t.Skip("Skipping IterResources tests due to deprectation: Set TEST_QUERY_PLAN_RESOURCES=true to enable")
-		}
 		runQueryPlanLookupResources(t, handle)
 	})
 
 	t.Run("lookup_subjects", func(t *testing.T) {
+		// LookupSubjects consistency is still gated: the query planner diverges from
+		// the dispatcher on wildcard-with-exclusion schemas (e.g. wildcardnested.yaml,
+		// publicwithexclusion.yaml). That is a separate defect from the recursion work
+		// and must be fixed before this gate can be removed. Set TEST_QUERY_PLAN_SUBJECTS=true
+		// to run it anyway.
 		if os.Getenv("TEST_QUERY_PLAN_SUBJECTS") == "" {
-			t.Skip("Skipping IterSubjects tests due to deprectation: Set TEST_QUERY_PLAN_SUBJECTS=true to enable")
+			t.Skip("Skipping IterSubjects consistency: known wildcard-exclusion divergence. Set TEST_QUERY_PLAN_SUBJECTS=true to enable")
 		}
 		runQueryPlanLookupSubjects(t, handle)
 	})
 }
 
 func runQueryPlanAssertions(t *testing.T, handle *queryPlanConsistencyHandle) {
-	if os.Getenv("TEST_QUERY_PLAN_CHECK") == "" {
-		t.Skip("Skipping Check tests due to deprecation. Set TEST_QUERY_PLAN_CHECK=true to enable")
-	}
 	t.Run("assertions", func(t *testing.T) {
 		for _, parsedFile := range handle.populated.ParsedFiles {
 			for _, entry := range []struct {
diff --git a/pkg/query/errors.go b/pkg/query/errors.go
new file mode 100644
index 0000000000..ed91f92661
--- /dev/null
+++ b/pkg/query/errors.go
@@ -0,0 +1,16 @@
+package query
+
+import "fmt"
+
+// MaxRecursionDepthError indicates that a recursive traversal did not resolve
+// within the configured maximum recursion depth. It mirrors the legacy
+// dispatcher's MaxDepthExceeded semantics: the answer is unknown, not negative.
+// Callers must surface this as an error rather than treating it as NOT_MEMBER or
+// an empty result set.
+type MaxRecursionDepthError struct {
+	Depth int
+}
+
+func (e MaxRecursionDepthError) Error() string {
+	return fmt.Sprintf("max recursion depth (%d) exceeded during recursive traversal: this usually indicates a recursive or too deep data dependency", e.Depth)
+}
diff --git a/pkg/query/reader.go b/pkg/query/reader.go
index 1d59d4099b..c53c00aec8 100644
--- a/pkg/query/reader.go
+++ b/pkg/query/reader.go
@@ -268,6 +268,11 @@ func (r *datalayerQueryDatastoreReader) SubjectExistsAsRelationship(
 	relIter, err := r.inner.QueryRelationships(ctx, filter,
 		options.WithLimit(&limitOne),
 		options.WithSkipExpiration(true),
+		// The filter pins the subject but leaves the resource columns open, which
+		// gaps the PK and makes CockroachDB reject a forced index hint. Varying lets
+		// the datastore pick an index from the actual filter columns (the subject
+		// index). This mirrors the reasoning in QuerySubjects above.
+		options.WithQueryShape(queryshape.Varying),
 	)
 	if err != nil {
 		return false, err
diff --git a/pkg/query/reader_test.go b/pkg/query/reader_test.go
new file mode 100644
index 0000000000..3765fb792b
--- /dev/null
+++ b/pkg/query/reader_test.go
@@ -0,0 +1,55 @@
+package query
+
+import (
+	"testing"
+
+	"github.com/stretchr/testify/require"
+
+	"github.com/authzed/spicedb/internal/datastore/dsfortesting"
+	"github.com/authzed/spicedb/internal/datastore/memdb"
+	"github.com/authzed/spicedb/internal/testfixtures"
+	"github.com/authzed/spicedb/pkg/datalayer"
+	"github.com/authzed/spicedb/pkg/tuple"
+)
+
+// recursiveUsersetSchema is the canonical "directly cyclic" userset relation.
+// The self-edge probe (SubjectExistsAsRelationship) only fires for schemas of
+// this shape, which is why the missing query shape went unnoticed.
+const recursiveUsersetSchema = `
+definition user {}
+definition group {
+	relation member: user | group#member
+}
+`
+
+// TestSubjectExistsAsRelationship_QueryShape verifies that the existence probe
+// specifies a query shape. Without it, the probe panics with "query shape is
+// unspecified" under the validating datastore that all testfixtures helpers wrap.
+func TestSubjectExistsAsRelationship_QueryShape(t *testing.T) {
+	require := require.New(t)
+
+	rawDS, err := dsfortesting.NewMemDBDatastoreForTesting(t, 0, 0, memdb.DisableGC)
+	require.NoError(err)
+
+	ds, revision := testfixtures.DatastoreFromSchemaAndTestRelationships(
+		t, rawDS, recursiveUsersetSchema,
+		[]tuple.Relationship{
+			tuple.MustParse("group:a#member@user:tom"),
+			tuple.MustParse("group:b#member@group:a#member"),
+		},
+	)
+
+	reader := NewQueryDatastoreReader(
+		datalayer.NewDataLayer(ds).SnapshotReader(revision, datalayer.NoSchemaHashForTesting),
+	)
+
+	// group:a appears as a subject of group:b#member, so the probe must find it.
+	exists, err := reader.SubjectExistsAsRelationship(t.Context(), NewObject("group", "a"), "member")
+	require.NoError(err)
+	require.True(exists)
+
+	// group:c never appears as a subject, so the probe must not find it.
+	exists, err = reader.SubjectExistsAsRelationship(t.Context(), NewObject("group", "c"), "member")
+	require.NoError(err)
+	require.False(exists)
+}
diff --git a/pkg/query/recursion_correctness_test.go b/pkg/query/recursion_correctness_test.go
new file mode 100644
index 0000000000..c2380a52ea
--- /dev/null
+++ b/pkg/query/recursion_correctness_test.go
@@ -0,0 +1,200 @@
+package query
+
+import (
+	"fmt"
+	"testing"
+
+	"github.com/stretchr/testify/require"
+
+	"github.com/authzed/spicedb/internal/caveats"
+	"github.com/authzed/spicedb/internal/datastore/dsfortesting"
+	"github.com/authzed/spicedb/internal/datastore/memdb"
+	"github.com/authzed/spicedb/internal/testfixtures"
+	caveattypes "github.com/authzed/spicedb/pkg/caveats/types"
+	"github.com/authzed/spicedb/pkg/datalayer"
+	"github.com/authzed/spicedb/pkg/tuple"
+)
+
+// compileRecursive writes the schema and relationships to a fresh datastore and
+// returns a query context (with a caveat runner) plus the compiled iterator for
+// the given definition and relation.
+func compileRecursive(t *testing.T, schemaText, def, relation string, rels []tuple.Relationship) (*Context, Iterator) {
+	t.Helper()
+
+	rawDS, err := dsfortesting.NewMemDBDatastoreForTesting(t, 0, 0, memdb.DisableGC)
+	require.NoError(t, err)
+
+	ds, revision := testfixtures.DatastoreFromSchemaAndTestRelationships(t, rawDS, schemaText, rels)
+
+	dsSchema, err := ReadSchema(t.Context(), ds, revision)
+	require.NoError(t, err)
+
+	outline, err := BuildOutlineFromSchema(dsSchema, def, relation)
+	require.NoError(t, err)
+	it, err := outline.Compile()
+	require.NoError(t, err)
+
+	reader := NewQueryDatastoreReader(datalayer.NewDataLayer(ds).SnapshotReader(revision, datalayer.NoSchemaHashForTesting))
+	ctx := NewLocalContext(t.Context(),
+		WithReader(reader),
+		WithCaveatRunner(caveats.NewCaveatRunner(caveattypes.Default.TypeSet)),
+		WithMaxRecursionDepth(defaultMaxRecursionDepth),
+	)
+	return ctx, it
+}
+
+// groupMemberSchema is the canonical directly-cyclic userset relation: a group's
+// members are users plus the members of nested groups.
+const groupMemberSchema = `
+definition user {}
+definition group {
+	relation member: user | group#member
+}
+`
+
+// buildGroupChain constructs `depth` nested groups g0..g(depth-1) where
+// g0#member@user:tom and g(i)#member@g(i-1)#member. Thus user:tom is transitively
+// a member of every group, reached only by walking the full chain.
+func buildGroupChain(t *testing.T, depth int) (*Context, Iterator) {
+	t.Helper()
+
+	rels := make([]tuple.Relationship, 0, depth)
+	rels = append(rels, tuple.MustParse("group:g0#member@user:tom"))
+	for i := 1; i < depth; i++ {
+		rels = append(rels, tuple.MustParse(fmt.Sprintf("group:g%d#member@group:g%d#member", i, i-1)))
+	}
+	return compileRecursive(t, groupMemberSchema, "group", "member", rels)
+}
+
+// TestDeepChainCheckErrorsRatherThanSilentlyDenying verifies that a Check whose
+// answer lies beyond MaxRecursionDepth returns an error, matching the legacy
+// engine's MaxDepthExceeded, rather than silently returning NOT_MEMBER.
+func TestDeepChainCheckErrorsRatherThanSilentlyDenying(t *testing.T) {
+	// The chain is longer than defaultMaxRecursionDepth (50), so the membership of
+	// user:tom in group:g59 cannot be determined within the depth budget.
+	ctx, it := buildGroupChain(t, 60)
+
+	_, err := ctx.Check(it, NewObject("group", "g59"), NewObject("user", "tom").WithEllipses())
+	require.Error(t, err, "a check beyond max recursion depth must error, not silently deny")
+	require.ErrorAs(t, err, &MaxRecursionDepthError{})
+}
+
+// TestShallowChainCheckSucceeds is the control: a chain within the depth budget
+// resolves normally, so the depth error is not spuriously raised.
+func TestShallowChainCheckSucceeds(t *testing.T) {
+	ctx, it := buildGroupChain(t, 10)
+
+	path, err := ctx.Check(it, NewObject("group", "g9"), NewObject("user", "tom").WithEllipses())
+	require.NoError(t, err)
+	require.NotNil(t, path, "user:tom is a member of group:g9 via the chain")
+}
+
+// TestDeepChainLookupResourcesErrorsRatherThanTruncating verifies that a
+// LookupResources whose full result set lies beyond MaxRecursionDepth errors
+// rather than silently returning a truncated set.
+func TestDeepChainLookupResourcesErrorsRatherThanTruncating(t *testing.T) {
+	ctx, it := buildGroupChain(t, 60)
+
+	paths, err := ctx.IterResources(it, NewObject("user", "tom").WithEllipses(), NoObjectFilter())
+	require.NoError(t, err)
+	_, err = CollectAll(paths)
+	require.Error(t, err, "an LR beyond max recursion depth must error, not silently truncate")
+	require.ErrorAs(t, err, &MaxRecursionDepthError{})
+}
+
+// TestShallowChainLookupResourcesSucceeds is the control for the LR path.
+func TestShallowChainLookupResourcesSucceeds(t *testing.T) {
+	ctx, it := buildGroupChain(t, 10)
+
+	paths, err := ctx.IterResources(it, NewObject("user", "tom").WithEllipses(), NoObjectFilter())
+	require.NoError(t, err)
+	results, err := CollectAll(paths)
+	require.NoError(t, err)
+	// user:tom is a member of all 10 groups g0..g9.
+	require.Len(t, results, 10)
+}
+
+// caveatedDiamondSchema allows a group's members to be reached via a caveated or
+// an uncaveated nested-group edge.
+const caveatedDiamondSchema = `
+definition user {}
+caveat cav1(v bool) { v }
+definition group {
+	relation member: user | group#member | group#member with cav1
+}
+`
+
+// caveatedDiamondRels forms a diamond a→{b,c}→...→tom where the short edge a→b is
+// caveated but the longer path a→c→b is not. user:tom is therefore an
+// UNCONDITIONAL member of group:a (via a→c→b→tom), so a correct Check must return
+// a nil caveat. The pre-fix implementation contaminates every descendant of b
+// with cav1, because b is first reached via the caveated edge and never
+// re-expanded once reached uncaveated.
+var caveatedDiamondRels = []tuple.Relationship{
+	tuple.MustParse("group:a#member@group:b#member[cav1]"),
+	tuple.MustParse("group:a#member@group:c#member"),
+	tuple.MustParse("group:c#member@group:b#member"),
+	tuple.MustParse("group:b#member@user:tom"),
+}
+
+// TestCaveatedDiamondCheckIsUnconditional is the core B1 soundness test: a subject
+// reachable by an uncaveated path must not be reported as conditionally reachable.
+func TestCaveatedDiamondCheckIsUnconditional(t *testing.T) {
+	ctx, it := compileRecursive(t, caveatedDiamondSchema, "group", "member", caveatedDiamondRels)
+
+	path, err := ctx.Check(it, NewObject("group", "a"), NewObject("user", "tom").WithEllipses())
+	require.NoError(t, err)
+	require.NotNil(t, path, "user:tom is a member of group:a")
+	require.Nil(t, path.Caveat, "membership is unconditional via a→c→b→tom; got caveat %v", path.Caveat)
+}
+
+// TestCaveatedDiamondIterSubjectsIsUnconditional checks the same soundness property
+// on the IterSubjects path: every descendant reachable uncaveated must be nil.
+func TestCaveatedDiamondIterSubjectsIsUnconditional(t *testing.T) {
+	ctx, it := compileRecursive(t, caveatedDiamondSchema, "group", "member", caveatedDiamondRels)
+
+	paths, err := ctx.IterSubjects(it, NewObject("group", "a"), NewType("user"))
+	require.NoError(t, err)
+	results, err := CollectAll(paths)
+	require.NoError(t, err)
+
+	require.Len(t, results, 1)
+	require.Equal(t, "tom", results[0].Subject.ObjectID)
+	require.Nil(t, results[0].Caveat, "user:tom is an unconditional member of group:a; got caveat %v", results[0].Caveat)
+}
+
+// TestCaveatedDiamondIterResourcesIsUnconditional checks the soundness property on
+// the IterResources (LookupResources) path: group:a is an unconditional resource
+// for user:tom via a→c→b→tom, so its path must carry a nil caveat.
+func TestCaveatedDiamondIterResourcesIsUnconditional(t *testing.T) {
+	ctx, it := compileRecursive(t, caveatedDiamondSchema, "group", "member", caveatedDiamondRels)
+
+	paths, err := ctx.IterResources(it, NewObject("user", "tom").WithEllipses(), NoObjectFilter())
+	require.NoError(t, err)
+	results, err := CollectAll(paths)
+	require.NoError(t, err)
+
+	byResource := make(map[string]*Path, len(results))
+	for _, p := range results {
+		byResource[p.Resource.ObjectID] = p
+	}
+	require.Contains(t, byResource, "a", "group:a must be a resource for user:tom")
+	require.Nil(t, byResource["a"].Caveat, "user:tom's membership in group:a is unconditional; got caveat %v", byResource["a"].Caveat)
+}
+
+// TestCaveatedCycleTerminates verifies the fixpoint converges on cyclic data with a
+// caveated edge — the canonical condition prevents unbounded caveat growth — and
+// still resolves the unconditional membership correctly.
+func TestCaveatedCycleTerminates(t *testing.T) {
+	rels := []tuple.Relationship{
+		tuple.MustParse("group:a#member@group:b#member[cav1]"),
+		tuple.MustParse("group:b#member@group:a#member"),
+		tuple.MustParse("group:a#member@user:tom"),
+	}
+	ctx, it := compileRecursive(t, caveatedDiamondSchema, "group", "member", rels)
+
+	path, err := ctx.Check(it, NewObject("group", "a"), NewObject("user", "tom").WithEllipses())
+	require.NoError(t, err)
+	require.NotNil(t, path, "user:tom is a direct member of group:a")
+	require.Nil(t, path.Caveat, "direct membership is unconditional; got caveat %v", path.Caveat)
+}
diff --git a/pkg/query/recursive.go b/pkg/query/recursive.go
index 0e898c723a..42d6c2dca9 100644
--- a/pkg/query/recursive.go
+++ b/pkg/query/recursive.go
@@ -33,9 +33,11 @@ func init() {
 // frontierEntry is a lightweight frontier node for BFS IterSubjects.
 // It carries only the fields needed to combine with the next hop's path —
 // unlike a full *Path it does not hold Resource, Relation, or Metadata.
+// Condition is the canonical caveat condition under which Subject was reached,
+// which is conjoined with each outgoing edge's caveat as the frontier advances.
 type frontierEntry struct {
 	Subject    ObjectAndRelation
-	Caveat     *core.CaveatExpression
+	Condition  caveats.Condition
 	Expiration *time.Time
 	Integrity  []*core.RelationshipIntegrity
 }
@@ -275,15 +277,24 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 	}
 
 	return func(yield func(*Path, error) bool) {
-		// Track yielded paths by endpoints for global deduplication with OR/caveat semantics.
+		// yieldedPaths accumulates every endpoint path, OR-merged by endpoint key.
+		// Results are buffered and flushed only once the traversal converges: under a
+		// caveated schema a later ply can weaken the condition on an already-seen
+		// endpoint (an object first reached via a caveated edge and later reached
+		// unconditionally), so emitting eagerly could leak a stale, over-restrictive
+		// caveat (bug B1). Buffering adds no memory — every path was retained here
+		// already for cross-ply deduplication.
 		yieldedPaths := make(map[string]*Path)
 
-		// Track queried objects to prevent cycles (avoid re-querying same objects).
-		queriedObjects := make(map[string]bool)
+		// reached records, for each object that has entered the frontier, the
+		// canonical caveat condition under which it was reached. An object is
+		// re-expanded only when a new path *weakens* that condition — the semi-naive
+		// fixpoint. Because the condition is canonical, conjunction is idempotent
+		// (c1 ∧ c2 ∧ c1 == {c1,c2}) and the unconditional case is absorbing under OR,
+		// so the fixpoint terminates even on cyclic data.
+		reached := make(map[string]caveats.Condition)
 
-		// frontier holds lightweight entries — just the fields needed to combine with the next
-		// hop's path. Using frontierEntry rather than *Path avoids keeping Resource, Relation,
-		// and Metadata alive across plies.
+		reached[resource.Key()] = caveats.Top()
 		frontier := []frontierEntry{
 			{
 				Subject: ObjectAndRelation{
@@ -291,9 +302,9 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 					ObjectID:   resource.ObjectID,
 					Relation:   tuple.Ellipsis,
 				},
+				Condition: caveats.Top(),
 			},
 		}
-		queriedObjects[resource.Key()] = true
 
 		// plyPaths is allocated once and cleared each ply to avoid per-ply allocations.
 		plyPaths := make(map[string]*Path)
@@ -315,7 +326,8 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 			clear(plyPaths)
 
 			// Query IterSubjects FROM each frontier object, accumulating results in plyPaths.
-			// Paths with the same endpoint from different frontier nodes are merged with OR.
+			// Each edge's caveat is conjoined with the condition under which the frontier
+			// object itself was reached; endpoints reached multiple ways this ply are ORed.
 			for _, fe := range frontier {
 				frontierResource := GetObject(fe.Subject)
 
@@ -340,11 +352,12 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 					//   fe:      original_resource → frontier_resource  (implicit)
 					//   subPath: frontier_resource → subject
 					//   result:  original_resource → subject
+					pathCondition := fe.Condition.And(caveats.FromExpression(subPath.Caveat))
 					combinedPath := &Path{
 						Resource:   resource,
 						Relation:   r.relationName,
 						Subject:    subPath.Subject,
-						Caveat:     caveats.And(fe.Caveat, subPath.Caveat),
+						Caveat:     pathCondition.Expression(),
 						Expiration: combineExpiration(fe.Expiration, subPath.Expiration),
 						Integrity:  combineIntegrity(fe.Integrity, subPath.Integrity),
 					}
@@ -365,7 +378,8 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 				ctx.TraceStep(r, "Ply %d: found %d unique paths", ply, len(plyPaths))
 			}
 
-			// Extract frontier objects collected by all sentinels during this ply.
+			// Extract frontier objects collected by all sentinels during this ply
+			// (arrow recursion surfaces its next hop this way rather than as subjects).
 			var collectedObjects []Object
 			for _, sentinelID := range sentinelIDs {
 				collectedObjects = append(collectedObjects, ctx.ExtractFrontierCollection(sentinelID)...)
@@ -376,13 +390,10 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 
 			// Reset and reuse nextFrontier.
 			nextFrontier = nextFrontier[:0]
-			yieldedCount := 0
 
+			// Merge this ply's endpoints into the global buffer and re-enqueue any
+			// recursive object whose reaching condition weakened.
 			for key, path := range plyPaths {
-				isRecursive := path.Subject.ObjectType == r.definitionName
-				matchesFilter := filterSubjectType.Type == "" ||
-					path.Subject.ObjectType == filterSubjectType.Type
-
 				if existing, seen := yieldedPaths[key]; seen {
 					if _, err := existing.MergeOr(path); err != nil {
 						yield(nil, err)
@@ -390,61 +401,73 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 					}
 				} else {
 					yieldedPaths[key] = path
-					if matchesFilter {
-						yieldedCount++
-						if !yield(path, nil) {
-							return
-						}
-					}
 				}
 
-				if isRecursive {
-					objKey := GetObject(path.Subject).Key()
-					if !queriedObjects[objKey] {
-						queriedObjects[objKey] = true
-						nextFrontier = append(nextFrontier, frontierEntry{
-							Subject:    path.Subject,
-							Caveat:     path.Caveat,
-							Expiration: path.Expiration,
-							Integrity:  path.Integrity,
-						})
-						if ctx.shouldTrace() {
-							ctx.TraceStep(r, "Ply %d: adding %s to next frontier", ply, objKey)
-						}
-					} else if ctx.shouldTrace() {
-						ctx.TraceStep(r, "Ply %d: skipping %s (already queried, cycle detected)", ply, objKey)
+				if path.Subject.ObjectType != r.definitionName {
+					continue
+				}
+
+				objKey := GetObject(path.Subject).Key()
+				newCondition, changed := reached[objKey].Or(caveats.FromExpression(path.Caveat))
+				if !changed {
+					if ctx.shouldTrace() {
+						ctx.TraceStep(r, "Ply %d: %s already reached under an equal-or-weaker condition", ply, objKey)
 					}
+					continue
+				}
+				reached[objKey] = newCondition
+				nextFrontier = append(nextFrontier, frontierEntry{
+					Subject:    path.Subject,
+					Condition:  newCondition,
+					Expiration: path.Expiration,
+					Integrity:  path.Integrity,
+				})
+				if ctx.shouldTrace() {
+					ctx.TraceStep(r, "Ply %d: (re)adding %s to next frontier", ply, objKey)
 				}
 			}
 
-			// Add sentinel-collected objects to the frontier.
+			// Add sentinel-collected objects to the frontier; they are unconditional.
 			for _, obj := range collectedObjects {
 				objKey := obj.Key()
-				if !queriedObjects[objKey] {
-					queriedObjects[objKey] = true
-					nextFrontier = append(nextFrontier, frontierEntry{
-						Subject: ObjectAndRelation{
-							ObjectType: obj.ObjectType,
-							ObjectID:   obj.ObjectID,
-							Relation:   tuple.Ellipsis,
-						},
-					})
+				newCondition, changed := reached[objKey].Or(caveats.Top())
+				if !changed {
 					if ctx.shouldTrace() {
-						ctx.TraceStep(r, "Ply %d: adding collected object %s to frontier", ply, objKey)
+						ctx.TraceStep(r, "Ply %d: skipping collected object %s (already unconditional)", ply, objKey)
 					}
-				} else if ctx.shouldTrace() {
-					ctx.TraceStep(r, "Ply %d: skipping collected object %s (already queried, cycle detected)", ply, objKey)
+					continue
+				}
+				reached[objKey] = newCondition
+				nextFrontier = append(nextFrontier, frontierEntry{
+					Subject: ObjectAndRelation{
+						ObjectType: obj.ObjectType,
+						ObjectID:   obj.ObjectID,
+						Relation:   tuple.Ellipsis,
+					},
+					Condition: caveats.Top(),
+				})
+				if ctx.shouldTrace() {
+					ctx.TraceStep(r, "Ply %d: adding collected object %s to frontier", ply, objKey)
 				}
 			}
 
 			if ctx.shouldTrace() {
-				ctx.TraceStep(r, "Ply %d: yielded %d matching paths, %d for next frontier",
-					ply, yieldedCount, len(nextFrontier))
+				ctx.TraceStep(r, "Ply %d: %d entries for next frontier", ply, len(nextFrontier))
 			}
 
 			if len(nextFrontier) == 0 {
 				if ctx.shouldTrace() {
-					ctx.TraceStep(r, "BFS completed (no frontier at ply %d)", ply)
+					ctx.TraceStep(r, "BFS converged at ply %d; flushing %d paths", ply, len(yieldedPaths))
+				}
+				// The traversal has converged: flush every buffered endpoint that
+				// matches the subject-type filter.
+				for _, path := range yieldedPaths {
+					if filterSubjectType.Type != "" && path.Subject.ObjectType != filterSubjectType.Type {
+						continue
+					}
+					if !yield(path, nil) {
+						return
+					}
 				}
 				return
 			}
@@ -454,9 +477,15 @@ func (r *RecursiveIterator) breadthFirstIterSubjects(ctx *Context, resource Obje
 			frontier, nextFrontier = nextFrontier, frontier[:0]
 		}
 
+		// Reaching here means the frontier was still non-empty after maxDepth plies;
+		// a converged traversal returns early above once nextFrontier is empty. The
+		// answer is therefore not fully determined, so surface an error rather than
+		// yielding a silently-truncated result set (matching the legacy engine's
+		// MaxDepthExceeded behavior).
 		if ctx.shouldTrace() {
 			ctx.TraceStep(r, "BFS terminated at max depth %d", maxDepth)
 		}
+		yield(nil, MaxRecursionDepthError{Depth: maxDepth})
 	}, nil
 }
 
@@ -491,11 +520,19 @@ func (r *RecursiveIterator) breadthFirstIterResources(ctx *Context, subject Obje
 	}
 
 	return func(yield func(*Path, error) bool) {
-		// Track all paths yielded (for deduplication with OR/caveat semantics).
+		// yieldedPaths buffers every resource path, OR-merged by endpoint key, and is
+		// flushed only once the traversal converges. As with IterSubjects, a resource
+		// first reached via a caveated path can later be reached unconditionally, so
+		// emitting eagerly would leak a stale, over-restrictive caveat (bug B1).
 		yieldedPaths := make(map[string]*Path)
 
-		// newPaths collects genuinely new paths each ply; reused across plies.
-		var newPaths []*Path
+		// reached records the canonical caveat condition under which each resource has
+		// been reached. A resource re-seeds the frontier only when its condition
+		// weakens — the semi-naive fixpoint that keeps caveats sound and terminates.
+		reached := make(map[string]caveats.Condition)
+
+		// frontier holds the paths whose condition weakened last ply; reused across plies.
+		var frontier []Path
 
 		// Start with the original tree (sentinel returns empty at ply 0).
 		currentTree := r.templateTree
@@ -512,8 +549,8 @@ func (r *RecursiveIterator) breadthFirstIterResources(ctx *Context, subject Obje
 				return
 			}
 
-			// Reset new-paths accumulator, reusing backing array.
-			newPaths = newPaths[:0]
+			// Reset the frontier accumulator, reusing backing array.
+			frontier = frontier[:0]
 
 			for path, err := range plySeq {
 				if err != nil {
@@ -521,46 +558,50 @@ func (r *RecursiveIterator) breadthFirstIterResources(ctx *Context, subject Obje
 					return
 				}
 
-				// Deduplicate by endpoint.
 				key := path.EndpointsKey()
 				if existing, seen := yieldedPaths[key]; seen {
-					// Already yielded — merge caveats with OR semantics but do NOT
-					// re-add to the frontier (it was already queried in a prior ply).
 					if _, err := existing.MergeOr(path); err != nil {
 						yield(nil, err)
 						return
 					}
 				} else {
-					// Genuinely new path — record, yield, and add to frontier.
 					pathCopy := *path
 					yieldedPaths[key] = &pathCopy
-					newPaths = append(newPaths, path)
-					if !yield(path, nil) {
-						return
-					}
 				}
+
+				// Re-seed the frontier only if this resource's reaching condition
+				// weakened; the frontier path carries the canonical accumulated
+				// condition so the next ply combines edges against the weakest form.
+				newCondition, changed := reached[key].Or(caveats.FromExpression(path.Caveat))
+				if !changed {
+					continue
+				}
+				reached[key] = newCondition
+				frontierPath := *path
+				frontierPath.Caveat = newCondition.Expression()
+				frontier = append(frontier, frontierPath)
 			}
 
 			if ctx.shouldTrace() {
-				ctx.TraceStep(r, "Ply %d: found %d new paths", ply, len(newPaths))
+				ctx.TraceStep(r, "Ply %d: %d frontier paths", ply, len(frontier))
 			}
 
-			// If no genuinely new paths, we've reached a fixed point.
-			if len(newPaths) == 0 {
+			// No condition weakened this ply: the fixpoint has converged. Flush the
+			// buffered results.
+			if len(frontier) == 0 {
 				if ctx.shouldTrace() {
-					ctx.TraceStep(r, "BFS completed (no new paths at ply %d)", ply)
+					ctx.TraceStep(r, "BFS converged at ply %d; flushing %d paths", ply, len(yieldedPaths))
+				}
+				for _, path := range yieldedPaths {
+					if !yield(path, nil) {
+						return
+					}
 				}
 				return
 			}
 
-			// Build Fixed iterator from new paths only (not already-queried paths).
-			derefed := make([]Path, len(newPaths))
-			for i, p := range newPaths {
-				derefed[i] = *p
-			}
-			fixedFrontier := NewFixedIterator(derefed...)
-
-			// Replace sentinel with Fixed frontier for next ply.
+			// Replace sentinel with the weakened frontier for the next ply.
+			fixedFrontier := NewFixedIterator(frontier...)
 			modifiedTree, err := r.replaceRecursiveSentinel(r.templateTree, fixedFrontier)
 			if err != nil {
 				yield(nil, fmt.Errorf("failed to replace sentinel: %w", err))
@@ -569,9 +610,13 @@ func (r *RecursiveIterator) breadthFirstIterResources(ctx *Context, subject Obje
 			currentTree = modifiedTree
 		}
 
+		// Reaching here means a condition was still weakening after maxDepth plies;
+		// a converged traversal returns early above. Surface an error rather than
+		// yielding a silently-truncated result set.
 		if ctx.shouldTrace() {
 			ctx.TraceStep(r, "BFS terminated at max depth %d", maxDepth)
 		}
+		yield(nil, MaxRecursionDepthError{Depth: maxDepth})
 	}, nil
 }
 
diff --git a/pkg/query/recursive_coverage_test.go b/pkg/query/recursive_coverage_test.go
index 2ac044493e..bcc54d234e 100644
--- a/pkg/query/recursive_coverage_test.go
+++ b/pkg/query/recursive_coverage_test.go
@@ -106,12 +106,12 @@ func TestBreadthFirstIterResources_MaxDepth(t *testing.T) {
 	seq, err := recursive.IterResourcesImpl(ctx, ObjectAndRelation{ObjectType: "user", ObjectID: "alice", Relation: "..."}, NoObjectFilter())
 	require.NoError(err)
 
-	paths, err := CollectAll(seq)
-	require.NoError(err)
-
-	// Should terminate at max depth, not infinite loop
-	// Each ply generates one new path, so we expect at most 3 paths
-	require.LessOrEqual(len(paths), 3, "Should terminate at max depth")
+	// The iterator never converges, so the traversal exhausts its depth budget.
+	// It must terminate with a MaxRecursionDepthError rather than either looping
+	// forever or silently returning a truncated result set.
+	_, err = CollectAll(seq)
+	require.Error(err, "Should terminate at max depth with an error, not silently truncate")
+	require.ErrorAs(err, &MaxRecursionDepthError{})
 }
 
 // TestBreadthFirstIterResources_ErrorHandling tests error paths in BFS IterResources