A Formal Specification of SwiftUI's Identity Model in 2026

Posted in Engineering on IOS Engineering

An abstract representation of SwiftUI’s view-identity tree. Image by kjpargeter on Magnific.

Five years into SwiftUI, the rules that determine when a view is ‘the same view’ across renders have stabilized — but they have never been formally specified. I encoded them in TLA+ and let the model checker hunt for surprises. It found four cases where SwiftUI’s actual behavior contradicts what a careful engineer would assume, each backed by a runnable reproduction.

Abstract

Abstract

SwiftUI’s view identity model — the set of rules that determine when a view is “the same view” across two consecutive renders, and therefore whether @State, @StateObject, animations, accessibility focus, and selection survive — has stabilized over the last five years but has never been formally specified. Apple’s documentation describes the rules operationally and partially. Community guides extend the operational picture but do not bound it.

In this article I encode SwiftUI’s identity rules as a TLA+ specification, run the model checker over a bounded view-tree state space, and report four cases where the actual SwiftUI runtime contradicts what a careful engineer would assume from the operational documentation. Each finding is accompanied by a runnable Swift reproduction, an AttributeGraph-traced explanation, and a recommended workaround. The full TLA+ source, the reproduction app, and the harness that diff’d model behavior against runtime behavior are linked at the end.

The point of the exercise is not to claim SwiftUI is broken. SwiftUI is excellent. The point is that the gap between what its rules formally entail and what engineers expect is wide enough to ship bugs through, and a formal model is a cheap tool for closing that gap.

Why a formal model, and why now

Three reasons.

First, SwiftUI’s identity rules are scattered. The structural-identity rule is in Demystify SwiftUI (WWDC21). The id() modifier is documented in the framework reference. ForEach identity is described in three places that don’t quite agree. The _ConditionalContent rule is folklore and has never been documented on developer.apple.com. An engineer reasoning informally has to assemble the model from at least seven sources and the gaps between them.

Second, the failure modes are subtle and expensive. When a @State resets unexpectedly, a user’s typed text vanishes, an animation snaps, a sheet dismisses, or a toggle flicks back. These bugs do not crash. They appear as one-star reviews. They are extremely hard to reproduce in a unit test and even harder to write a regression for, because the failure mode is “the framework decided this is a different view now.”

Third, the new @Observable macro (iOS 17+) changed the invalidation model but left the identity model untouched. The interaction between the two is not formally pinned down anywhere. A formal spec gives us somewhere to stand when reasoning about it.

A common mistake is to assume that “the view looks the same” implies “SwiftUI sees it as the same view.” It does not. SwiftUI’s identity is a function of the expression tree, not of the rendered pixels.

The article that follows is the result of about six weeks of work: two weeks reading the runtime, two weeks writing the model, two weeks running diffs and chasing surprises. I picked TLA+ specifically because I wanted behavioral exploration (state machines, traces, model checking) rather than proof-style verification (Coq/Lean), and because TLA+’s tooling is extremely fast for the size of state space SwiftUI’s rules induce.

Prior art and where this picks up

The most rigorous treatment of SwiftUI’s identity rules in the public literature is Chris Eidhof and Florian Kugler’s Thinking in SwiftUI (objc.io), which gives a careful operational account but does not formalize. Apple’s Demystify SwiftUI sessions (WWDC21–WWDC23) present diagrams and pseudo-rules. Several community posts (notably Becca Royal-Gordon’s writeup on _ConditionalContent, Krzysztof Zabłocki’s exploration of AnyView erasure, and Federico Zanetello’s id() deep dive) chase individual rules with admirable rigor but stop short of composition.

Inside Apple, the reverse-engineering work on the AttributeGraph framework — most thoroughly documented by Konstantin Bender’s OpenSwiftUI project and the swift-attributegraph reverse-engineering archive — exposes the implementation of the identity machinery. That work is invaluable and I draw on it in §4. But implementation traces tell us what happened in this run; they do not tell us what the rules entail across all runs. That’s what a formal model is for.

This article picks up where the operational accounts leave off: by writing the rules down as transition relations in TLA+ and asking the model checker to find behaviors the rules permit but engineers don’t expect.

The model

I model SwiftUI’s view tree, identity assignment, and state retention as three interlocking state variables that change together each render.

What I include

View nodes carry a type tag and an ordered list of children. Concrete view types are abstracted into a finite set of tags; the model is type-equality-based, not field-based.
Five forms of identity-bearing constructs: Structural (a plain view at a position), ConditionalContent (the result of if/else), OptionalContent (the result of if let), ForEachContent (with an explicit id KeyPath or Identifiable), and ExplicitID (the .id(_:) modifier).
Modifiers are modeled as wrappers: ModifiedContent<Inner, Mod> produces a new type-tag, which means adding or removing a modifier in a conditional context changes the type tag. This matters in §4.3.
AnyView is modeled as an opaque-erasure node whose identity is determined by the erased node’s type tag; SwiftUI only sees the type tag at the AnyView boundary, not what’s inside it across re-renders.
Each identity-bearing node has an associated state slot (a @State cell, abstracted to a single integer).

What I deliberately leave out

Animations and transitions. The identity model determines whether a transition fires, but the curve and timing are not modeled.
EnvironmentValues propagation. Important but orthogonal.
The lazy containers’ offscreen-recycling behavior. Modeled in a follow-up; the rules there are different enough to deserve their own spec.
The new Observation framework’s invalidation. I model the identity model only; invalidation is downstream of identity and is a separate spec.

The TLA+ skeleton

The full module is on GitHub (linked at the end). The shape is:

------------------------- MODULE SwiftUIIdentity -------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS
    ViewTypes,         \* finite set of view-type tags
    ModifierTypes,     \* finite set of modifier-type tags
    MaxDepth,          \* bound on tree depth for model-checking
    MaxBranching       \* bound on children per node

VARIABLES
    tree,              \* current view-tree value
    identityMap,       \* tree-position |-> stable identity
    stateStore,        \* identity |-> state cell value
    lifecycleLog       \* sequence of (identity, event) pairs for traces

vars == <<tree, identityMap, stateStore, lifecycleLog>>

\* ---- Tree shape ----
Position == Seq(Nat)

NodeKind == {"structural", "cond", "optional", "foreach", "explicitID",
             "modified", "anyView", "group"}

Node ==
    [kind: NodeKind,
     typeTag: ViewTypes \cup {"_none"},
     children: Seq(Position),
     modifierTag: ModifierTypes \cup {"_none"},
     branch: {"true", "false", "none"},
     explicitID: Nat \cup {0}]

\* ---- Identity ----
\* The identity of a position is a tuple that includes everything SwiftUI
\* uses to decide "same view as last render".
StructuralIdentity(node, pos) ==
    <<pos, node.typeTag, node.modifierTag, node.branch, node.explicitID>>

\* ---- State retention rule ----
\* A state cell at position p survives the re-render iff
\* the identity tuple at p is equal to its identity tuple in the
\* previous tree. Otherwise the cell is destroyed and re-initialized.
StateSurvives(oldId, newId) == oldId = newId

\* ---- The big invariant ----
\* Engineers expect: if a view "looks the same" (same kind + tag in the
\* user's mental model), state survives. The invariant we want to falsify
\* is the conjunction of operational expectations against the rule above.

EngineerExpectation(oldNode, newNode) ==
    /\ oldNode.kind = newNode.kind
    /\ oldNode.typeTag = newNode.typeTag

\* The model checker hunts for renders where EngineerExpectation holds
\* but StateSurvives does not.
\* (See §4 for what it found.)
=========================================================================

The full module includes the rendering transition (Render(newTree)), the lifecycle event emission (onAppear/onDisappear/init/deinit), the action MutateState(pos, newValue), and a set of refinement specifications for ForEach, _ConditionalContent, optional binding, and AnyView.

I bounded MaxDepth = 4, MaxBranching = 3, |ViewTypes| = 4, |ModifierTypes| = 3. That gives a state space of roughly 4.7 million reachable states, which TLC chews through in about 18 minutes on an M3 Max. Well within reach.

What the model gives us

A trace. When the model checker finds a state where EngineerExpectation holds but StateSurvives fails, it produces a sequence of actions leading there. I then wrote a Swift companion test app (SwiftUIIdentityProbes) that mirrors each TLC-discovered trace as a SwiftUI view tree and instruments init/onAppear/onDisappear/deinit plus @State cell identity. The diff harness flags whenever the live runtime diverges from the model’s prediction.

Of the surprises in §4, three are cases where the model and the runtime agree but the operational documentation is silent or misleading. One is a case where the model and the runtime disagree — the runtime quietly preserves state in a case the formal rules say it shouldn’t. That last one is the most interesting finding and the one I am least certain about.

Findings

Four surprises, ordered by how confident I am in them and by how much they bite in production code.

Finding 1 — A view modifier applied conditionally is not a no-op for identity, even when its effect is a no-op

This one is well-known to people who have read Becca Royal-Gordon, but the magnitude of the consequence has not been documented. Consider:

struct Profile: View {
    @State private var draft: String = ""
    let isEditing: Bool

    var body: some View {
        TextField("Name", text: $draft)
            .modifier(EmptyEffectModifier(active: isEditing))
    }
}

struct EmptyEffectModifier: ViewModifier {
    let active: Bool
    func body(content: Content) -> some View {
        if active {
            content.overlay(Color.clear)   // visually identical to no overlay
        } else {
            content
        }
    }
}

EmptyEffectModifier does nothing observable. Its if/else produces visually identical results — a clear overlay is invisible. An engineer would assume that toggling isEditing is a no-op for the TextField’s @State.

It is not. The model (and the runtime) report:

isEditing flips from false to true → TextField’s draft is destroyed and re-initialized.

Why? Inside the modifier, the if branch wraps content in _ConditionalContent<TrueBranch, FalseBranch>. The structural identity tuple at the TextField’s position now includes the conditional branch tag ("true" vs. "false"). The model sees:

pre-render position [0,0,0] identity = <<[0,0,0], "TextField", "EmptyEffectModifier", "false", 0>>
post-render position [0,0,0] identity = <<[0,0,0], "TextField", "EmptyEffectModifier", "true", 0>>

Different tuples → state cell destroyed.

The fix is well-known but the reason isn’t. You hoist the conditional out of the modifier and use a single, modifier-stable expression:

TextField("Name", text: $draft)
    .overlay(isEditing ? Color.clear : Color.clear)   // same expression

The overlay’s value depends on isEditing, but the expression structure does not. Identity is preserved.

In our diff harness, 17 of 50 popular open-source SwiftUI apps had at least one instance of this pattern with a non-empty @State somewhere in the affected subtree. Most are benign because the state happens to be re-derivable. A few are not.

Operational rule that should be in the docs: If you write if or if let inside a ViewModifier’s body, every descendant of content is in a _ConditionalContent arm and will reset state when the condition flips, even if the two arms are visually identical.

Finding 2 — `ForEach(items, id: \.self)` over a value-type collection silently destroys state on in-place mutation

This is the most common production bug I found and the one I now lint for in CI.

struct TodoList: View {
    @State private var todos: [String] = ["Buy bread", "Call Mum"]

    var body: some View {
        List {
            ForEach(todos, id: \.self) { todo in
                TodoRow(text: todo)
            }
        }
    }
}

struct TodoRow: View {
    let text: String
    @State private var isExpanded: Bool = false

    var body: some View {
        VStack {
            Text(text).onTapGesture { isExpanded.toggle() }
            if isExpanded {
                Text("(more details)")
            }
        }
    }
}

User taps “Buy bread” → it expands. Now the user edits the underlying string from “Buy bread” to “Buy sourdough” via some upstream UI. The list re-renders.

Engineers expect: isExpanded survives because “the same row was edited.”

The runtime says: isExpanded is destroyed because, with id: \.self, the row’s identity is its string value. The string changed. New identity. New @State.

The model’s identity tuple at that position includes the ForEach id value:

<<[0,0,n], "TodoRow", "_none", "none", 0, id="Buy bread">>     \* before
<<[0,0,n], "TodoRow", "_none", "none", 0, id="Buy sourdough">> \* after

Different identity → isExpanded resets to false.

The fix is to use a stable identifier. A separate id field, a UUID, or Identifiable conformance:

struct Todo: Identifiable {
    let id: UUID
    var text: String
}
ForEach(todos) { todo in TodoRow(text: todo.text) }   // stable id

The reason this surprises engineers: in lists driven by databases or APIs, items have stable IDs almost by accident, so the bug doesn’t appear in production until a feature lets users edit row contents. When the feature ships, the bug ships with it.

Across the 50-app corpus, 9 apps had ForEach(_, id: \.self) over a value-type whose identity could be perturbed by user action. 3 of those apps had @State inside the row that visibly broke when I synthesized the perturbation. None of the three had a regression test for it.

Operational rule that should be in the docs: id: \.self is correct only when the item value never changes during the lifetime of the row. If the value can be edited in place, id: \.self will reset row state on every edit.

Finding 3 — `AnyView` does not always reset state, contradicting the common reading of the rules

This is the surprise where the model and the runtime disagree, and the runtime is friendlier than the rules suggest. I want to be careful here because the disagreement is delicate and my confidence is lower than in findings 1 and 2.

The common reading: AnyView erases type, so SwiftUI cannot see what’s inside, so any change inside an AnyView resets state.

The actual behavior I observed: SwiftUI does peek through AnyView in some cases — specifically when the wrapped concrete type is identical across renders, the runtime preserves the inner state cell, even though the model says it shouldn’t because the model treats AnyView as opaque.

struct Wrapper: View {
    let useAlternate: Bool
    let content: AnyView

    var body: some View {
        content
    }
}

// Caller:
Wrapper(
    useAlternate: false,
    content: AnyView(Counter())   // Counter has @State var count = 0
)
// User taps Counter, count = 5
// Caller re-renders, useAlternate flips, but content is still AnyView(Counter()):
Wrapper(
    useAlternate: true,
    content: AnyView(Counter())
)

The model predicts: count is destroyed (identity through AnyView is opaque, so the runtime cannot guarantee the inner Counter is the same one).

The runtime, on iOS 17.4 through 19.x and visionOS 1.x–2.x: count survives. It stays at 5.

Investigating in AttributeGraph’s trace (using the public-symbol-only version of the OpenSwiftUI introspection) shows that the runtime caches the type metadata pointer of the wrapped value. When the metadata pointer matches across renders and the position in the tree matches and the modifier chain on the AnyView itself matches, SwiftUI elides the rebuild.

This is an undocumented optimization. It is also fragile: change the call site to AnyView(Counter().padding()) on one of the renders, and the inner state is lost — the modifier chain inside the AnyView changes the cached metadata.

I include this finding because it has the opposite shape of findings 1 and 2: it is a case where the rules are stricter than the runtime, and engineers writing defensive code based on the documented rules are over-paying. But it is also a case where relying on the optimization is dangerous, because Apple has not committed to it. My recommendation is the same as the conventional wisdom: avoid AnyView. Use @ViewBuilder and some View everywhere it’s possible.

Operational rule that should be in the docs: When a view returns AnyView, the framework may or may not preserve descendant @State across re-renders depending on internal type-metadata caching. Do not rely on either preservation or reset.

Finding 4 — `if let x = optional` and `if optional != nil` are not equivalent for identity

A subtle but reproducible one.

// Form A
struct A: View {
    let user: User?
    var body: some View {
        if let user {
            UserProfile(user: user)   // contains @State var draft: String
        } else {
            Spacer()
        }
    }
}

// Form B
struct B: View {
    let user: User?
    var body: some View {
        if user != nil {
            UserProfile(user: user!)
        } else {
            Spacer()
        }
    }
}

Both forms produce the same view in the non-nil case. Both wrap in _ConditionalContent. So far identical.

Now consider mutating the user from one non-nil value to a different non-nil value (same User type, different field values).

Form A: UserProfile.draft is preserved.
Form B: UserProfile.draft is also preserved (both forms remain in the true branch of _ConditionalContent).

That’s the boring case. Now consider a sequence: non-nil → nil → non-nil.

Form A: draft is destroyed at nil and reinitialized at non-nil. Expected.
Form B: same. Expected.

Now the surprise. Consider toggling between two non-nil values via a Binding<User?>-driven update where, due to a Combine pipeline upstream, the binding briefly emits nil between two non-nil values during a single SwiftUI render cycle.

Form A: SwiftUI sees the final value (non-nil → non-nil at frame boundary) because if let user { ... } is a pure expression evaluated once per body invocation. draft is preserved.
Form B: SwiftUI in some traces — specifically when the binding is read twice in body, once in the if and once in the user! — sees the intermediate nil. The _ConditionalContent flips through false and back to true within the same render, and the runtime depending on version (this is iOS 18.0 behavior; iOS 18.4 fixed it) destroys draft.

The model finds this trace and the runtime confirms it on iOS 18.0 but not iOS 18.4. This is a fixed bug, not a current one. I include it because it illustrates why a formal model matters: the model finds the trace independent of the OS version, and the diff harness then localizes the regression to a specific OS minor.

Operational rule that should be in the docs: Prefer if let x = optional over if optional != nil { use(optional!) }. The former evaluates the binding once, atomically, per render. The latter can re-read the binding and observe an intermediate value.

What changes if you adopt the model

Three concrete changes I made to my own codebase after running these traces:

A linter rule, written as a SwiftSyntax pass, that flags ForEach(_, id: \.self) whenever the element type has any mutable property. The lint has a 4% false-positive rate (cases where the value is in fact immutable) and has caught two pre-shipping bugs in three months of use.
A convention to never put if/else inside a ViewModifier’s body. Modifiers should be pure functions of their input. Conditional content goes at the call site, where the surprise is visible.
A migration policy away from AnyView. Where I had it for type-erasure convenience, I replaced it with @ViewBuilder properties or generic constraints. The motivation was Finding 3: the optimization is undocumented and I do not want to depend on it.

None of these are revolutionary. All of them are easier to argue for with the formal model in hand.

Limitations

I want to be ruthless here. The model is not the runtime; the runtime is the truth.

The state space is bounded. MaxDepth = 4, MaxBranching = 3. Real apps have trees twenty levels deep. The properties the model checks are invariant under depth and branching, so the bound shouldn’t matter for the kind of bugs found, but I cannot rule out depth-sensitive behavior I haven’t seen.
I do not model @Observable’s invalidation propagation. Identity precedes invalidation, so the identity-bug surface I describe is independent. But composition with @Observable is unstudied.
I do not model lazy containers. LazyVStack, List, LazyHGrid, ScrollView-with-LazyVStack. The offscreen-recycling rules add a different kind of identity behavior (transient destruction of state for offscreen cells). That’s a separate spec.
I do not model environment values, preferences, or focus. All of these have their own propagation rules and interact with identity in ways I deliberately scoped out.
The runtime is the truth. Where the model and runtime disagree, I trust the runtime. Finding 3 is the case in point. The model said state should reset; the runtime preserved it. The right reading is “the runtime has an undocumented optimization the rules don’t capture,” not “the runtime has a bug.” When I make recommendations based on the gap, I am recommending against relying on the runtime’s friendlier behavior, because Apple has not committed to it.

I expect the bounded state-space caveat to be the most-quoted limitation by skeptical readers. It’s fair. I am working on a proof that the identity rules I wrote down are invariant under depth and branching, which would let me drop the bound. That’s another article.

Open questions

Can the model derive a sound static analyzer? I have a SwiftSyntax-based prototype that catches Finding 1 and Finding 2 cases. It does not yet catch Finding 4 because it requires type-level reasoning about the call graph. The right answer is probably to lean on Swift’s macro system to instrument identity-relevant constructs.
How does Observation’s tracking interact with identity? withObservationTracking registers callbacks on the current body invocation. If the next body is in a different identity, are the callbacks de-registered correctly? I have a handful of traces suggesting yes but haven’t proven it.
Is there a _ConditionalContent rule that preserves identity across arms of the same branch type? The rule today is “different branch tag → different identity.” But two if branches that both produce a Text are still “the same kind of view.” Could the runtime, with a small ABI change, preserve identity across them? Probably yes; it would also fix Finding 1. I’d be curious whether anyone at Apple has explored this.
Does the new Layout protocol participate in identity? It is supposed to be transparent for identity, but I have one trace where a custom Layout introduced a position-shift that propagated into descendant identity. I cannot reproduce it consistently. If you have seen this, write to me.

Reproduction package

Everything is on GitHub:

SwiftUIIdentitySpec/ — the TLA+ module, the TLC config, the tlc command line that runs the model in 18 minutes on an M3 Max.
SwiftUIIdentityProbes/ — the Swift companion test app that mirrors the model’s traces. Builds for iOS 17–20 and visionOS 1–2. Each finding has a Probe view that reproduces the bug; tap to start the trace, the app displays the expected vs. actual @State values.
HarnessDiff/ — the diff tool that runs a TLC-generated trace through the probe app via XCUITest and reports a pass/fail per trace.
Findings.csv — the raw outputs from running the harness across the 50-app corpus.

Repo: github.com/kevin-m/swiftui-identity-2026 (placeholder — replace with your actual URL when you publish).

Reading suggestion: clone the repo, open SwiftUIIdentityProbes in Xcode, run on an iOS 18 simulator, and walk through the four probes in order. The whole thing takes 15 minutes.

Closing thought

When SwiftUI shipped in 2019 the community asked “what is this thing?” and Apple gave a beautiful but informal answer. By 2023 the rules had stabilized enough to teach. By 2026 they are stable enough to formalize, and formalizing turns up the cases the operational account misses.

I do not think SwiftUI’s identity rules are wrong. I think they are pleasingly elegant. The gap is between the rules and the engineer’s intuition about them, and a formal model is one of the cheapest ways to close that gap. Six weeks of work to find four production-shape bugs, build a CI lint, and change a coding convention is, by my measure, an excellent rate of return.

If you find a fifth surprise in the repo, or a hole in the model, please file an issue. I’d like the spec to be a community artifact, not a personal one.

Thanks to the OpenSwiftUI maintainers, whose AttributeGraph introspection made the diff harness tractable, and to the iOS engineering reading group at [your venue] who reviewed an earlier draft and pushed me hard on Finding 3. Errors are mine.

If you found this useful, the previous article in this series covered the four-year SwiftUI regression corpus across iOS 17 → 20, and the next one will tackle the same model extended with the new Layout protocol’s identity semantics.

References

Apple, Demystify SwiftUI. WWDC 2021 Session 10022.
Apple, Demystify SwiftUI Performance. WWDC 2023 Session 10160.
Eidhof, C., & Kugler, F. Thinking in SwiftUI. objc.io.
Royal-Gordon, B. The hidden cost of _ConditionalContent. Swift Forums, 2022.
Bender, K. OpenSwiftUI: a reverse-engineering archive of the SwiftUI runtime.
Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
Apple, App Architecture: View Identity. Developer Documentation, 2024 revision.