# Realizing: Spec + Manifest → Running Code

Deep dive on how `spv realize` turns a `.specly` spec and a manifest into production code. Covers the pipeline, manifest structure, instance factories, capability resolution, the L1/L2/L3 generation levels, the behavior generation walkthrough, and the instance factory catalog.

**See also:**
- [SPECVERSE-INTRO.md](SPECVERSE-INTRO.md) — philosophy and ecosystem overview
- [SPECVERSE-SPECIFYING.md](SPECVERSE-SPECIFYING.md) — write the specs that `realize` operates on
- [SPECVERSE-TOOLING.md](SPECVERSE-TOOLING.md) — the `spv realize` CLI surface
- [SPECVERSE-EXTENDING.md](SPECVERSE-EXTENDING.md) — add a new instance factory, a new LLM provider, formal verification with Quint
- [SPECVERSE-ARCHITECTURE.md](SPECVERSE-ARCHITECTURE.md) — internal architecture of the realize engine

---

## Contents

- [The Pipeline](#the-pipeline)
- [Manifests](#manifests)
- [Instance Factories](#instance-factories)
- [Capability Resolution](#capability-resolution)
- [Generation Levels (L1 – L4)](#generation-levels-l1--l4)
- [The Behavior Generation Walkthrough](#the-behavior-generation-walkthrough)
- [Step Resolution Priority](#step-resolution-priority)
- [The Promotion Lifecycle](#the-promotion-lifecycle)
- [Instance Factory Catalog](#instance-factory-catalog)
- [Generated Output Structure](#generated-output-structure)
- [Regeneration Safety (Factory B / ReactAppStarter)](#regeneration-safety-factory-b--reactappstarter)

---

## The Pipeline

Realize is the third and final stage of the SpecVerse pipeline.

```
.specly spec          # WHAT (from SPECVERSE-SPECIFYING)
    ↓
[parse + infer]       # → inferred spec with controllers, services, events, views
    ↓
manifest YAML         # HOW (technology choices)
    ↓
[spv realize]
    ↓
generated code        # Backend + Frontend + CLI + Tools (depending on manifest)
```

The key insight: **spec defines WHAT, manifest defines HOW.** Same spec → change manifest → different technology stack. Swap Fastify for NestJS, Prisma for TypeORM, React for Vue — the `.specly` doesn't change, only the manifest and the instance factory mappings.

---

## Manifests

Manifests bridge the logical spec to concrete technology. They declare:

1. Which deployment in the spec to realize
2. Which instance factories to use
3. How capabilities map to those factories
4. Default technology choices
5. Per-instance overrides

### Manifest Structure

```yaml
# manifests/implementation.yaml
specVersion: "5.1.1"
version: "1.0.0"
name: "MyApp Implementation"
description: "Next.js + PostgreSQL implementation"

# REQUIRED: link to the deployment in your spec
deployment:
  deploymentSource: "./specs/main.specly"
  deploymentName: "production"

# Instance factories for code generation
instanceFactories:
  - name: "FastifyPrismaAPI"
    source:
      type: "npm"
      package: "@specverse/engines"
      entrypoint: "libs/instance-factories/applications/fastify-prisma.yaml"

  - name: "ReactAppRuntime"
    source:
      type: "npm"
      package: "@specverse/engines"
      entrypoint: "libs/instance-factories/applications/react-app-runtime.yaml"

  - name: "PrismaPostgres"
    source:
      type: "npm"
      package: "@specverse/engines"
      entrypoint: "libs/instance-factories/orms/prisma-postgres.yaml"

# Default technology mappings
defaults:
  controller: "FastifyAPI"
  storage: "PostgreSQL15"
  view: "ReactAppRuntime"

# Capability-to-instance-factory mappings
capabilityMappings:
  - capability: "api.rest.crud"
    instanceFactory: "FastifyPrismaAPI"
  - capability: "storage.database"
    instanceFactory: "PrismaPostgres"
  - capability: "view.webapp"
    instanceFactory: "ReactAppRuntime"

# Override specific instances with custom mappings (optional)
overrides:
  - instance: "UserController"
    type: "controller"
    capability: "api.rest.crud"
    customInstanceFactory: "CustomUserAPI"
```

### How realize resolves the manifest

```
spec + manifest
    ↓
[loader]              — parses both files
    ↓
[resolver]            — for each instance in the deployment:
    ↓                   1. look up the capability it requires
    ↓                   2. find the mapped factory
    ↓                   3. load the factory's YAML + TypeScript generator
    ↓
[code generator]      — executes each factory template:
    ↓                   1. builds a context (spec + model + manifest)
    ↓                   2. calls the generator function with the context
    ↓                   3. writes the generated file
    ↓
generated code tree
```

**Manifest resolution order** (when `-m` not specified to `spv realize`):
1. If `-m <path>` provided: use that manifest file
2. Otherwise: look for `manifests/implementation.yaml` in current directory
3. If not found: error (no default manifest assumed)

---

## Instance Factories

Instance factories are the fundamental unit of code generation. Each factory is a YAML file declaring what it produces, plus a set of TypeScript generator templates.

### Factory Structure

A factory YAML declares:
- **name** and **version** — factory identity
- **category** — controller, service, view, storage, etc.
- **capabilities** — what it provides (`api.rest.crud`) and what it requires (`storage.database`)
- **technology** — runtime, language, framework, database
- **codeTemplates** — pointers to generator functions that produce code
- **dependencies** — runtime, dev, and peer dependencies for the generated project
- **configuration** — default values the factory uses
- **requirements** — environment variables and files the generated code needs

### Factory Execution

```
manifest capability → resolver → factory YAML → code template → TypeScript generator
                                                                      ↓
                                                              context { spec, model, manifest, ... }
                                                                      ↓
                                                                output { code, filePath }
                                                                      ↓
                                                                written to output directory
```

### Capability-Based Architecture

Factories advertise capabilities like `api.rest.crud`, `storage.database`, `orm.schema`, `view.webapp`. The manifest maps these capabilities to factories. This means:

- **Swap technologies by changing capability mappings** — no factory modifications, no spec changes
- **Add a new factory** — it advertises the capabilities it provides, and manifests can choose it
- **Add a new capability** — declare it in the schema, write a factory that provides it, map it in manifests

This is what enables **Define Once, Implement Anywhere**.

---

## Capability Resolution

Capabilities are kebab-case strings describing what a factory provides or requires.

### Standard Capability Taxonomy

| Domain | Capabilities |
|---|---|
| **API** | `api.rest`, `api.rest.crud`, `api.graphql`, `api.grpc` |
| **Storage** | `storage.database`, `storage.keyvalue`, `storage.blob`, `storage.queue`, `storage.search` |
| **ORM** | `orm.schema`, `orm.migrations`, `orm.client` |
| **View** | `view.webapp`, `view.native`, `view.admin`, `view.embedded` |
| **Service** | `service.business`, `service.integration`, `service.notification`, `service.lifecycle` |
| **Communication** | `communication.pubsub`, `communication.rpc`, `communication.queue`, `communication.streaming` |
| **Security** | `security.auth`, `security.authz`, `security.encryption`, `security.audit` |
| **Infrastructure** | `infra.loadbalancer`, `infra.gateway`, `infra.cdn`, `infra.dns`, `infra.ingress` |
| **Monitoring** | `monitoring.metrics`, `monitoring.logging`, `monitoring.tracing`, `monitoring.alerting` |
| **Testing** | `testing.unit`, `testing.integration`, `testing.e2e` |
| **Tools** | `tools.cli`, `tools.mcp`, `tools.vscode` |
| **SDK** | `sdk.typescript`, `sdk.python` |

### Resolution Flow

```
deployment instance
  .type = "controllers"
  .provider = (not specified; resolved via capability)

    ↓

resolver.resolveCapability("api.rest.crud")

    ↓

matching factory = manifest.capabilityMappings["api.rest.crud"]
                 = "FastifyPrismaAPI"

    ↓

factory = library.get("FastifyPrismaAPI")
        = {
            name: "FastifyPrismaAPI",
            capabilities: { provides: ["api.rest", "api.rest.crud"] },
            codeTemplates: { routes: { generator: "..." }, services: { ... } }
          }
```

Then the code generator executes the factory's templates with the inferred spec as context.

---

## Generation Levels (L1 – L4)

SpecVerse generates code at four levels of sophistication, each building on the last. Most generators stop at L1; SpecVerse goes through L3 as standard, with L4 as a discovery mechanism.

### L1: Structural Scaffolding

Scaffold-level output. Correct structure, placeholder logic.

- Models → ORM schema classes
- Controllers → CURVED route stubs (endpoints declared, handlers empty)
- Views → component skeletons with empty JSX

This is what most code generators do. SpecVerse does it as a baseline.

### L2: Convention-Based

Convention patterns produce **real working code**, not stubs. Each pattern maps a specification construct to a concrete implementation step:

- Model attributes → typed ORM columns with constraints
- Relationships → foreign keys with cascade rules
- Lifecycle flows → state machine implementations with transition validation
- CURVED operations → route handlers with request validation
- Events → typed pub/sub with payload schemas

The same convention patterns apply regardless of target technology. Change the manifest from Prisma to TypeORM, and the conventions produce equivalent output for the new ORM.

### L3: Behavioural (Formal)

Business logic that goes beyond structural patterns. The realize engine translates declarative behaviors in the spec into runtime TypeScript with:

- **Preconditions** — guards that must pass before an operation executes
- **Postconditions** — assertions about state after an operation completes
- **Event emissions** — domain events triggered by state changes
- **Quint transpilation** — formal specifications in Quint (a TLA+ successor) are transpiled into TypeScript runtime guard functions

**Two distinct Quint surfaces — do not conflate them:**

- **Validate-time spec invariants.** The entity-module Quint specs (`__behaviour__/*.qnt`) are transpiled and run by `spv validate --verify` to check that *the spec itself* is well-formed (relationship targets exist, lifecycle states are non-empty, etc.). These run **at validation time against the spec**, *in-process*, and emit **nothing** into the generated backend. On the self-spec, raw shows 7/7 invariants hold and inferred shows 14/14.
- **Runtime constraint guards.** When a model declares `constraints: [{on, requires}]`, realize emits a per-model `<Model>.guards.ts` (see [The Constraint Generation Walkthrough](#the-constraint-generation-walkthrough) below), invoked inside the controller's `validate()`. This is the **only** Quint-derived logic that runs **at runtime in the generated backend** — it is narrow (the constraint sugar vocabulary) and **fails open** (a guard that throws is treated as PASS).

Formal tooling: Quint specs are **type-checked** with `quint typecheck` (a build-time gate that skips if the binary is absent). Full **Apalache model-checking is not currently wired** — see the decision in [`docs/proposals/in-progress/2026-05-30-QUINT-FORMAL-LAYER-DECISION.md`](../proposals/in-progress/2026-05-30-QUINT-FORMAL-LAYER-DECISION.md).

### L4: AI-Generated (Discovery)

No template or formal spec covers the requirement. An LLM generates code from the specification context. This is where complex business logic, domain-specific algorithms, and integration glue live. The output works but isn't yet proven reusable.

AI-generated outputs are cached in `.specverse/ai-cache/` keyed on `sha256(step + model + operation + inputs + promptVersion)` so re-running `spv realize` with unchanged inputs is free.

### Cost projection: `spv realize --estimate`

Before committing to a full generation (which can take minutes and cost LLM tokens), `--estimate` reports expected output broken down by layer:

```bash
spv realize all specs/main.specly --estimate -m manifests/implementation.yaml
```

Output sample (a 7-entity codebase):

```
spv realize --estimate
  L1 — Instance factory (templates, no LLM):           ~97 files
  L2 — Convention pattern matching (CURVED + events): 44 ops
  L3 — AI from steps (LLM call per declared step):    32 calls
       (23 model-behavior steps + 9 service-op steps)

  Estimated cost:
    Max subscription:    ~7 min wallclock, $0.00 marginal
    Sonnet API:          ~7 min, ~$0.48
    DeepSeek:            ~5 min, ~$0.026
```

This makes L3 commitment explicit — investors and engineers see exactly what costs when before the first token spends.

### Multi-component realize fan-out

When a spec declares multiple components (e.g. `idle-meta` with 8 domain components: AuthDomain / PlayerDomain / GameDomain / ...), realize merges all components' map sections (models / controllers / services / events / views / primitives / enums / lifecycles) into one flat code generation. This was a known limitation prior to engines 6.3.0 — earlier versions silently dropped all components except the first, leaving multi-component specs partially-realized. Now: 8-component idle-meta yields 11 controllers / 34 services / 5 `*.ai.ts` behavior files with library references preserved end-to-end through to function headers.

---

## The Behavior Generation Walkthrough

This is L3 in action. Given this spec:

```yaml
behaviors:
  processPayment:
    parameters:
      paymentMethod: String required
      amount: Money required
    requires: ["Order exists", "Amount matches order total"]
    ensures: ["Payment recorded", "Order status updated"]
    publishes: [PaymentProcessed]
    steps:
      - "Validate payment details"
      - "Charge payment provider"
      - "Record transaction"
      - "Update order status to paid"
```

The generator produces:

```typescript
async processPayment(paymentMethod: string, amount: number): Promise<void> {
    // === PRECONDITIONS ===
    const order = await this.prisma.order.findUnique({ where: { id: params.id } });
    if (!order) throw new Error('Precondition failed: Order exists');
    if (params.amount !== params.orderTotal) {
      throw new Error('Precondition failed: Amount matches order total');
    }

    // === EXECUTE ===
    // Step 1: Validate payment details
    const validationResult = this.validate(params, { operation: 'processPayment' });
    if (!validationResult.valid) {
      throw new Error(`Validation failed: ${validationResult.errors.join(', ')}`);
    }

    // Step 2: Charge payment provider
    // (No convention match — stub generated)
    await this.chargePaymentProvider(params);

    // Step 3: Create transaction record
    const transaction = await this.prisma.transaction.create({ data: params });

    // Step 4: Update order status to paid
    await this.prisma.order.update({
      where: { id: params.id },
      data: { status: 'paid' },
    });

    // === POSTCONDITIONS (dev-mode) ===
    if (process.env.NODE_ENV === 'development') {
      console.assert(true, 'POSTCONDITION: Payment recorded');
      console.assert(true, 'POSTCONDITION: Order status updated');
    }

    // === EVENTS ===
    this.emit('PaymentProcessed', { operation: 'processPayment', timestamp: new Date().toISOString() });
}

// Generated stub — compiles, throws at runtime
private async chargePaymentProvider(params: any): Promise<void> {
    throw new Error('Not implemented: chargePaymentProvider');
}
```

**Steps 1, 3, and 4 are convention-matched** (real code). **Step 2 has no matching pattern, so it gets a stub** method that compiles but throws — the developer implements only the genuinely novel logic.

### What maps to convention patterns

15 common patterns generate real code:

| Step text | Generated code |
|---|---|
| "Validate payment details" | Validation call with error throwing |
| "Find order by id" | ORM lookup with not-found guard |
| "Update order status to paid" | ORM update with field assignment |
| "Create transaction record" | ORM create from params |
| "Transition order to shipped" | Lifecycle-aware status update |
| "Increment stock by quantity" | Atomic increment with underflow guard |
| "Send PaymentProcessed event" | Event emission with context |
| "Call InventoryService.reserve" | Service method delegation |
| "Check sufficient stock" | Guard method with lookup |
| "Calculate total from items" | Calculator helper method |

### Quint actions for formal guarantees

> **Status (2026-05-30): designed, not currently wired.** The `transpileActions` transpiler exists, but the
> realize step-resolver does not invoke it (live resolution is convention → AI → stub), and there is no
> author-`.qnt` loader in the pipeline. This section documents an *intended* capability, not a working feature.
> See [`docs/proposals/in-progress/2026-05-30-QUINT-FORMAL-LAYER-DECISION.md`](../proposals/in-progress/2026-05-30-QUINT-FORMAL-LAYER-DECISION.md)
> for the wire-it-or-retire-it decision.

For complex business logic, the intent is that you can write **Quint action specifications** alongside your `.specly` file. Quint actions are formally verifiable and transpile to TypeScript:

```quint
action confirmOrder(order, paymentId): bool = all {
  order.status == "pending",                // guard → precondition check
  paymentId != "",                          // guard → precondition check
  order' = { ...order, status: "confirmed", confirmedAt: now() },  // effect → ORM update
  emit(OrderConfirmed, { orderId: order.id, paymentId }),          // event → emission
}
```

Transpiles to:

```typescript
async confirmOrder(params: { id: string; paymentId: string }): Promise<void> {
    // === GUARDS ===
    if (!(order.status === "pending")) {
      throw new Error('Guard failed: order.status == "pending"');
    }
    if (!(paymentId !== "")) {
      throw new Error('Guard failed: paymentId != ""');
    }

    // === EFFECTS ===
    await this.prisma.order.update({
      where: { id: params.id },
      data: { status: 'confirmed', confirmedAt: new Date() },
    });

    // === EVENTS ===
    this.emit('OrderConfirmed', { orderId: params.id, paymentId: params.paymentId });
}
```

(When wired, the intent is that the Quint action is type-checked via `quint typecheck` before transpilation. Apalache model-checking is **not** currently integrated — see the status note above.)

---

## The Constraint Generation Walkthrough

Parallel to behaviors, **model constraints** (declared via `model.constraints: [{on, requires}]` — see [Constraints in SPECVERSE-SPECIFYING](SPECVERSE-SPECIFYING.md#constraints)) flow through their own emit pipeline. The author-written sugar becomes a Quint `pure def` becomes a TypeScript guard function, which the controller invokes inside `validate()`.

Given this spec:

```yaml
models:
  Vote:
    attributes:
      choice: String required
    relationships:
      voter: belongsTo User
      poll:  belongsTo Poll
    constraints:
      - on: [create]
        requires: "Poll is open"
      - on: [create, update]
        requires: "Vote's choice is set"
```

The realize cycle emits **a new sibling file** `Vote.guards.ts` next to `VoteController.ts`:

```typescript
// Auto-generated — DO NOT EDIT
import type { ConstraintRecord, Violation } from './guards-types.js';

export const MODEL_CONSTRAINTS: ConstraintRecord[] = [
  {
    on: ["create"],
    guard: (self: any, actor: any) => self.poll.votingStatus === "open",
    name: "guard_Poll_is_open",
    source: "Poll is open",
  },
  {
    on: ["create", "update"],
    guard: (self: any, actor: any) => self.choice !== null,
    name: "guard_Vote_choice_is_set",
    source: "Vote's choice is set",
  },
];

export function matchesOp(constraintOn: string[], op: string): boolean { /* ... */ }

export function runGuards(input: any, op: string, actor: any = null): Violation[] {
  const violations: Violation[] = [];
  for (const c of MODEL_CONSTRAINTS) {
    if (!matchesOp(c.on, op)) continue;
    let passed = true;
    try {
      passed = c.guard(input, actor);
    } catch (e: any) {
      // Fail-OPEN: log loudly, do NOT block the mutation. A throw indicates
      // a guard-internal defect (transpile bug, undefined path traversal,
      // type mismatch) rather than a real constraint failure.
      console.error(
        `[runGuards] constraint "${c.name}" (source: ${c.source}) threw during op="${op}" — treating as PASS:`,
        e?.stack ?? e?.message ?? e,
      );
      continue;
    }
    if (!passed) {
      violations.push({
        constraint: c.name,
        scope: op,
        source: c.source,
        message: `Constraint "${c.source}" failed`,
      });
    }
  }
  return violations;
}
```

And `VoteController.ts` gains a `runConstraintGuards` import + invocation inside its `validate()`:

```typescript
import { runGuards as runConstraintGuards } from './Vote.guards.js';

export class VoteController {
  public validate(
    _data: any,
    _context: { operation: 'create' | 'update' | 'evolve' | 'delete' | `evolve.${string}` },
    _actor: any = null,
  ): { valid: boolean; errors: string[] } {
    const errors: string[] = [];
    // ...attribute-level validation...

    // Constraint guards matching this operation
    const constraintViolations = runConstraintGuards(_data, _context.operation, _actor);
    for (const v of constraintViolations) errors.push(v.message);

    return { valid: errors.length === 0, errors };
  }

  public async create(data: any, _actor: any = null): Promise<any> {
    const validationResult = this.validate(data, { operation: 'create' }, _actor);
    if (!validationResult.valid) {
      throw new Error(`Validation failed: ${validationResult.errors.join(', ')}`);
    }
    // ...prisma create...
  }
  // ... update / delete / evolve all thread _actor identically ...
}
```

### Actor wiring (Slice 14)

The Fastify route handler reads `request.user` (decorated by `@fastify/jwt`, a custom `preHandler`, or any auth middleware) and threads it through:

```typescript
// In VoteRoutes.ts — auto-generated
fastify.post('/api/votes', {
  handler: async (request, reply) => {
    try {
      const _actor = (request as any).user ?? null;
      const vote = await handler.create(request.body as any, _actor);
      return reply.status(201).send(vote);
    } catch (error) { /* ... */ }
  },
});
```

When no auth middleware is wired, `request.user` is undefined and `_actor` is null. Constraints referencing `actor.*` paths will throw (e.g. `actor.role === "admin"` on a null actor), which the fail-open policy catches — the operation proceeds and the throw is logged. This is intentional: it means you can ship the spec without auth, layer auth in later, and the realized backend never breaks.

### The 5 enforcement modes — how `runGuards` plugs in

Each mode consumes constraint metadata differently. `runGuards` is the **server-side enforcement** (mode γ via the `/validate` route handler + the actual mutation handler). The other four modes happen client-side via `@specverse/runtime`:

| Mode | Where it runs | What it consumes |
|---|---|---|
| α — FK dropdown filter | Browser (runtime/views/react `annotateFkOptions`) | `model.constraints[on:'create']` evaluated locally against each FK option's parent |
| γ — Server preflight | Server (this section's `runGuards` via `POST /api/<plural>/validate`) | Full constraint set; returns 422 with violations on failure |
| δ — Button disable | Browser (`checkLocalPermission`) | `model.constraints[on:'create']` evaluated locally against selected parent |
| ε — Error display | Browser consumes server response | `runGuards` violations become `FormViolationsPanel` rows + `FieldError` inline + `ValidationToast` |
| ζ — Pending checks | Browser (`collectPendingChecks`) | Constraints that the local 3-valued evaluator can't decide (subqueries, actor refs) — shown informationally |

The schema endpoint at `/api/models/:name/schema` exposes the constraints array verbatim so the browser modes can build their views.

### Internals — where the emission lives

| File | Role |
|---|---|
| `entities/src/_shared/behaviour/convention-processor.ts` | Recognizes the 9 sugar conventions; produces a Quint AST node |
| `engines/src/inference/quint-transpiler.ts` | `transpilePhase2Guard(name, params, body)` → TS function body with `===` strict-equality upgrade |
| `engines/libs/instance-factories/services/templates/_shared/guards-generator.ts` | Emits the per-model `<Model>.guards.ts` (MODEL_CONSTRAINTS table + runGuards runtime). Shared across all 3 ORMs (prisma / mongodb-native / postgres-native) |
| `engines/libs/instance-factories/services/templates/{prisma,mongodb-native,postgres-native}/controller-generator.ts` | Adds the import + `runConstraintGuards` call inside `validate()`; widens method signatures with `_actor: any = null` |
| `engines/libs/instance-factories/controllers/templates/fastify/routes-generator.ts` | Extracts `const _actor = (request as any).user ?? null` in each mutation handler |

Unconstrained models emit byte-identical output to pre-Phase-2 — the controller still accepts `_actor` (so route handlers don't need per-model branching), but `MODEL_CONSTRAINTS` is empty and `runConstraintGuards` is never called.

### Slice 15a — Create-time relation loading

When `model.constraints` reference a `belongsTo` traversal (e.g. `self.poll.votingStatus == "open"` on Vote), the realized `create()` method needs the loaded Poll entity in `self.poll` BEFORE calling `validate()`. Otherwise `self.poll` is undefined (Create's input data only has `pollId`, not the loaded relation), the guard throws, and the fail-open policy lets the mutation through unchecked.

Each ORM controller-generator emits a load block when the model has constraints AND belongsTo rels:

```typescript
public async create(data: any, _actor: any = null): Promise<any> {
  // Phase 2 Slice 15a — load belongsTo relations from input FKs before
  // validate so guards traversing self.<rel> see the related entity.
  const __loadedRels: Record<string, any> = {};
  if (data.pollId) {
    __loadedRels.poll = await prisma.poll.findUnique({ where: { id: data.pollId } });
  }
  if (data.voterId) {
    __loadedRels.voter = await prisma.user.findUnique({ where: { id: data.voterId } });
  }
  const __mergedSelf = { ...data, ...__loadedRels };
  const validationResult = await this.validate(__mergedSelf, { operation: 'create' }, _actor);
  // ...
}
```

Helpers per ORM: `generateBelongsToLoad` (prisma), `generateMongoBelongsToLoad` (mongo), `generatePgBelongsToLoad` (postgres). Mirrors the Slice 8 Update-self-from-DB pattern. Models without constraints OR without belongsTo rels emit the unchanged simple form.

### Slice 15b — Async guards + ctx threading (subqueries)

The verb subquery sugar (`{Actor} has not {verb} on {Target}`) emits TS like `Vote.exists(...)` where `Vote` is an undefined identifier — just a Quint Set reference left over from transpile. Without intervention this throws → fail-open → duplicate votes get through.

Fix at the guards-generator layer (`rewriteSubqueriesAsync` helper): detects bare-Capitalized `.some(...)` patterns post-transpile, rewrites them:

```typescript
// Before (fails at runtime):
export function guard(self, actor): boolean {
  return ! Vote.some((__v: any) => __v.voterId === actor.id && __v.pollId === self.pollId);
}

// After (15b rewrite):
export async function guard(self, actor, ctx?: any): Promise<boolean> {
  const __Vote = ctx?.query?.('Vote');
  if (!__Vote) return true; // fail-open: no ctx → skip subquery
  return ! await __Vote.exists((__v: any) => __v.voterId === actor.id && __v.pollId === self.pollId);
}
```

Cascade:
- `runGuards` becomes `async`; awaits each guard call (uniformly wraps sync + async)
- Controllers' `validate()` becomes async; builds inline `__guardCtx` with per-model query helpers (prisma `findMany().some(predicate)`, mongo `find({}).toArray().some(...)`, postgres `findAll(model).some(...)`)
- All `this.validate(...)` callers `await` the result
- Fastify routes-generator `await`s `handler.validate(...)` in the validate handler

### Slice 15c — App-demo interpreter constraint enforcement

The dynamic interpreter (app-demo) doesn't go through `spv realize`, so the emitted `<Model>.guards.ts` files don't exist there. A separate evaluator JIT-compiles each constraint body using the same Quint→TS pipeline:

```typescript
// src/runtime/engine/constraint-evaluator.ts
import { transpilePhase2Guard } from '@specverse/engines/inference';

class ConstraintEvaluator {
  compile(constraint) {
    const transpiled = transpilePhase2Guard(name, params, body);
    // Same subquery rewrite logic as guards-generator
    // ... wraps in `new Function('self', 'actor', 'ctx', src)`
  }
}
```

`DynamicModelStore.enforceConstraints` runs on every create/update/delete/evolveLifecycle. Loads belongsTo relations from the in-memory store (mirrors 15a). Builds in-memory `ctx.query` that backs subquery sugars with store scans. Threads actor via `dynamic-controller-engine.ts` from `{id: context.userId}`. Result: app-demo's dynamic interpreter enforces the SAME constraints as the realized backend, against the same Quint bodies, with the same fail-open contract.

### Slice 15e — Hard-fail parser on unresolvable constraints

A constraint that can't expand (typo'd field, missing lifecycle, unknown sugar) was previously pushed to `warnings[]` + silently dropped — the spec loaded with weaker enforcement than the author intended. Now it's a hard error: `convention-processor.ts` collects to `errors[]`; `unified-parser.ts` rolls into `parseResult.errors`; spec loaders (e.g. app-demo's `SpecLoader`) throw + refuse to start. Message names the model + constraint + reason.

---

## Step Resolution Priority

When the realize engine encounters a step in a behavior, it resolves it in this priority order:

1. **Quint action** — *(designed, not currently wired — see the status note under "Quint actions for formal guarantees" above; the resolver does not check for author Quint actions today)*
2. **Convention pattern** — one of 15 common patterns generates real code
3. **AI-generated body** — an `aiBehaviors.<fn>()` call filled by the LLM (L4)
4. **Stub method** — compiles but throws `Not implemented` at runtime

Each `requires` becomes a runtime guard that throws on failure. Each `ensures` becomes a dev-mode assertion. Each `publishes` becomes an event emission. Helper methods generated by conventions and stubs are appended to the service class automatically.

---

## The Promotion Lifecycle

The four generation levels form a **maturity progression**. Every piece of generated code starts somewhere on this curve and can move up:

```
AI-Generated (L4)     →  verify & test  →  Formal (L3)  →  extract pattern  →  Convention (L2)  →  templatize  →  Template (L1)
  LLM produces code                          Quint/Lean spec                      15 reusable                       deterministic
  from spec + context                        model-checked                        patterns                          zero-ambiguity
```

**The key insight: AI is the discovery mechanism for new deterministic patterns.** Every successful AI-generated solution is a candidate for promotion:

```
Unknown requirement
    ↓
AI generates a solution (L4)
    ↓ verify with tests
Solution works, extract the pattern
    ↓ formalize with Quint
Pattern is formally verified (L3)
    ↓ extract to convention
Convention pattern added to engine (L2)
    ↓ templatize
Instance factory with deterministic output (L1)
```

This creates a **self-improving ecosystem.** The more specs are written and AI-generated solutions are verified, the more patterns graduate to deterministic generation. The formal verification layer (Quint) is the promotion gate — only verified patterns become conventions.

In practice:
- The 15 convention patterns started as hand-written code, observed across multiple projects, then codified
- The Quint guards started as informal preconditions, then were formalized and model-checked
- Future: AI-generated service implementations that pass test suites get extracted into new convention patterns

This is what distinguishes SpecVerse from both traditional code generators (which only do L1) and AI coding assistants (which only do L4). The maturity curve means the system gets **more deterministic over time**, not more dependent on AI.

### When to pick each level

- **Most specs**: just declare `requires` and `steps` — the realize engine picks the best available implementation (Quint → convention → stub)
- **Critical business logic**: write a Quint action spec alongside your `.specly` — get formally verified guards
- **Novel requirements**: let the AI pane in [app-demo](SPECVERSE-APP-DEMO.md) generate a first pass, then promote the pattern once it's proven

---

## Instance Factory Catalog

The realize engine ships with factories for a complete stack, organized by category under `engines/libs/instance-factories/`:

### Backend

| Factory | Technology | What it generates |
|---|---|---|
| `controllers/fastify` | Fastify | Route handlers per model, server bootstrap with auto-wired routes, health endpoint |
| `services/prisma` | Prisma | CURVED controllers with lifecycle validation, business logic services, L3 behavior generation |
| `orms/prisma` | Prisma | `schema.prisma` from models (relations, types, defaults, FK types, lifecycle status fields) |
| `validation/zod` | Zod | Validation schemas per model, JSON Schema for Fastify |
| `communication/eventemitter` | EventEmitter3 | Event bus, typed publishers, subscriber registration |
| `communication/websocket` | ws | WebSocket bridge with auto-reconnect + React-StrictMode-safe lifecycle |

### Frontend

View rendering is driven by the framework-agnostic walker in `@specverse/runtime/views/core` + the React adapter in `@specverse/runtime/views/react` + the Tailwind renderer in `@specverse/runtime/views/tailwind`. Two application factories consume this pattern library:

| Factory | Technology | What it generates |
|---|---|---|
| `applications/ReactAppRuntime` | React + Vite | Slim shell (~10 files) that imports `@specverse/runtime` and renders views at browser runtime |
| `applications/ReactAppStarter` | React + Vite | Fully standalone starter kit — per-view `.tsx` components, no `@specverse/runtime` dep, regeneration-safe via content hashing |

The `ReactAppRuntime` path is the default. Use `spv init --static` (or set the manifest's `app.frontend` capability to `ReactAppStarter`) to pick the starter-kit variant. See [SPECVERSE-VIEW-RENDERING.md](SPECVERSE-VIEW-RENDERING.md) for the full "one pattern library, three consumers" architecture.

### CLI and Tools

| Factory | Technology | What it generates |
|---|---|---|
| `cli/commander` | Commander.js | CLI entry point, command files from spec's `commands:` section |
| `tools/vscode` | VS Code API | Extension with 14 commands, tmLanguage grammar, themes, schema validation |
| `tools/mcp` | MCP SDK | MCP server with services, spec-driven tool/resource registry |

### Infrastructure and Deployment

| Factory | Technology | What it generates |
|---|---|---|
| `scaffolding/generic` | — | `package.json`, `tsconfig`, `.env`, `.gitignore`, README |
| `infrastructure/docker-k8s` | Docker, Kubernetes | Dockerfiles, `docker-compose.yml`, Kubernetes manifests |
| `storage/postgresql` | PostgreSQL | Config + Docker setup |
| `storage/mongodb` | MongoDB | Config + Docker setup |
| `storage/redis` | Redis | Config + Docker setup |
| `testing/vitest` | Vitest | Test suites (unit, integration, e2e) |

### SDKs

| Factory | Technology | What it generates |
|---|---|---|
| `sdks/typescript` | TypeScript | Type-safe API client SDK |
| `sdks/python` | Python | aiohttp + Pydantic API client SDK |

**Swap factories by changing the manifest** — the spec stays the same. Add a new factory (see [SPECVERSE-EXTENDING.md](SPECVERSE-EXTENDING.md)) to target a new technology.

---

## Generated Output Structure

A single `spv realize all` produces a complete project. The exact structure depends on your manifest, but the typical output is:

```
generated/
├── backend/
│   ├── src/
│   │   ├── main.ts              # Server entry point
│   │   ├── routes/              # Route handlers per model
│   │   ├── services/            # Business logic with L3 behaviors
│   │   ├── controllers/         # CURVED controllers
│   │   └── <Model>.guards.ts    # Per-model constraint guards — ONLY if the model declares constraints:
│   ├── prisma/
│   │   ├── schema.prisma        # ORM schema from models
│   │   └── migrations/
│   └── package.json
├── frontend/                    # (if manifest includes a view factory)
│   ├── src/
│   │   ├── App.tsx              # App shell with navigation
│   │   ├── components/          # (ReactAppStarter only) List, detail, form views per model
│   │   └── api/                 # Type-safe API client
│   └── package.json
├── cli/                         # (if spec defines commands)
│   └── src/
├── tools/                       # (if manifest includes tools factories)
│   ├── vscode-extension/
│   └── specverse-mcp/
└── schema/                      # SPECVERSE-SCHEMA.json for validation
```

### Standalone output layouts

When the manifest declares `app.frontend: false` (backend-only) or `app.backend: external` (frontend-only), the realize loop gates on resolved capabilities:

- **backend-only**: no `frontend/` dir, no `tests/contract/`, no React tsconfig, no `dev.specly`. Flat backend at the output root.
- **frontend-only**: no `backend/` dir, no `prisma/`, no server wiring. Flat frontend at the output root.

These are controlled by the manifest's `outputStructure` setting and the `app.frontend` capability resolution in `engines/src/realize/index.ts`.

---

## Regeneration Safety (Factory B / ReactAppStarter)

The `ReactAppStarter` factory is the "starter kit" variant — it emits a full React codebase the user can edit freely. To prevent regeneration from clobbering edits, it uses **content hashing**:

1. At every generation, the factory writes an SHA-256 hash of each file it produces to `.specverse-gen/hashes.json`
2. On the next `spv realize`:
   - For each file the factory would emit, compute the hash of what's currently on disk
   - If the disk hash matches the recorded "last-generated" hash → the user hasn't touched it. Safe to overwrite with the new rendering
   - If the disk hash differs → the user edited the file. Skip it with a warning:
     > `⚠  Skipped src/views/PostListView.tsx — user-edited since last generation.`
     > `   Run \`spv realize --force PostListView\` to overwrite, or delete the file to opt into regeneration.`
   - For files that don't exist yet → write them and record the hash as usual
3. Update the manifest with hashes of all written files

**The user's mental model:** *"files I've touched won't be overwritten; files I haven't are fair game."* No merge conflicts, no surprises. If they want to adopt an upstream pattern change for a file they've edited, they delete their local copy and regenerate.

The `.specverse-gen/` directory sits alongside the generated code and is checked into version control. Deleting it causes the next `spv realize` to treat all files as user-edited (safe default — never clobber work).

---

## Related

- [SPECVERSE-INTRO.md](SPECVERSE-INTRO.md) — the documentation hub
- [SPECVERSE-SPECIFYING.md](SPECVERSE-SPECIFYING.md) — write the specs that realize consumes
- [SPECVERSE-TOOLING.md](SPECVERSE-TOOLING.md) — `spv realize` CLI surface
- [SPECVERSE-EXTENDING.md](SPECVERSE-EXTENDING.md) — add new instance factories, LLM providers, Quint specs
- [SPECVERSE-VIEW-RENDERING.md](SPECVERSE-VIEW-RENDERING.md) — the "one pattern library, three consumers" frontend architecture
- [SPECVERSE-ARCHITECTURE.md](SPECVERSE-ARCHITECTURE.md) — internal architecture of the realize engine