Record Layers

Each record layer rests on the one above it: Behavior fulfills Intent, Implementation builds Behavior, and Proof proves Implementation. Derivation between records is part of that direction, so generic refusals derive from access and input without new records. An agent either writes the missing record above such code or removes the code, so the specification wins where Intent has spoken.

An agent that finds a guard in code with no record above it writes the requirement or rule, or removes the guard.

Checked bylitespec model check emits no behavior-unrecorded finding for a refusal literal, a screen call to no endpoint, or an engine step mapping to no use case, and reports mark-missing for a code element that carries no mark.

Marked checkable: the tool named here checks it.

Intent promises outcomes in product words, and Behavior turns each promise into the states, invariants, refusals, consistency, data classes with erasure positions, freshness, and tenant-scoped access that keep it. Only Behavior records fulfill a requirement (litespec/core/intent#restrict-requirement-fulfillment-to-behavior). Without that detail each implementer guesses the states and the access scope, and two guesses diverge. The checks requirement-fulfillment-missing, record-link-missing, step-use-case-missing, erasure-undeclared, and setting-requirement-missing report the gaps.

A reimbursement promise gains an entity with Approved and Reimbursed states, a refusal for an expense that is already reimbursed, and atomic consistency over one aggregate.

Checked bylitespec model check emits no requirement-fulfillment-missing, record-link-missing, step-use-case-missing, erasure-undeclared, or setting-requirement-missing finding across Behavior records.

Marked checkable: the tool named here checks it.

The model page holds the one list of figures the owner sets: prices, fees, rates, terms, markets, payers, retention periods, freshness, and figures that differ by tenant, market, or date. Each figure is a business choice, and only an accountable person makes it. An agent that fixed one would bury a commitment in a Behavior record nobody chose. The figure becomes a question to the owner or a backlog item, never a silent default.

A receipt threshold of EUR 25 waits for the owner instead of entering the setting silently.

Reviewed forWhich figures the owner sets did Behavior fix without asking? Look at the settings and rules the change adds, beside the list of owner-set figures on the model page.

Marked guidance: a reviewer answers this question.

The stack pages fix the code shapes, so the handler, the repository call, and the published event each have one prescribed form. An observable outcome, edge, write, or access grant outside the records splits the project into a specification that says one thing and code that does another. The checks behavior-unrecorded, write-undeclared, result-undeclared, effect-undeclared, and refusal-unimplemented report the excess, and analyzer LS2012 reports a handler that authorizes itself.

A handler that returns a code no result declares fails result-undeclared; the fix declares the result or removes the code.

Checked bylitespec model check emits no behavior-unrecorded, write-undeclared, result-undeclared, effect-undeclared, or refusal-unimplemented finding across the implementation.

Marked checkable: the tool named here checks it.

Small projects carry no scenarios unless the bdd extension switches them on, so the rule binds large projects and small projects with the extension. A scenario is the leaf of the record tree, so one test through the public boundary ties each leaf to running behavior. The checks use-case-scenario-missing and proves-unreached report the missing proof.

Checked bylitespec model check emits no use-case-scenario-missing or proves-unreached finding across scenarios and tests.

Marked checkable: the tool named here checks it.

The lower record layer does not decide what the upper record layer left unstated, so the need travels up with its context instead of turning into a guess. A question to the owner settles what only an accountable person decides, and a backlog item holds the rest where it stays visible. The specification is closed: an agent builds what it states and nothing more.

A missing reimbursement policy becomes a question to the owner, not a rule the agent writes.

Reviewed forWhich unstated needs lack a question to the owner or a backlog item? Look at the added records from a lower record layer, beside the owner questions and the backlog.

Marked guidance: a reviewer answers this question.

Commitments flow down, and facts from the world flow up: a provider's behavior, a regulation, or an incident enters Intent where people can weigh it. The citation and date show where the fact came from and when it held, so a later change rechecks the source instead of the memory.

An observed two-day payout settlement window enters as research, then as a constraint citing that research.

Reviewed forWhich world facts entered without a cited and dated research or constraint record? Look at the provider, regulation, and incident facts the change relies on.

Marked guidance: a reviewer answers this question.

A production incident ships its fix at once, at 02:00 if that is when the page fires. The incident exception records what shipped and why, and the records are updated before it expires. An expired exception is a blocking finding, so the gap stays visible until the records close it.

Reviewed forWhich incident fixes lack an exception, or carry an expired one? Look at the exception records beside each fix.

Marked guidance: a reviewer answers this question.

The provider's behavior is a fact from the world, and research is where such facts enter. The constraint that follows cites the research, so the constraint carries its evidence. Code is not the source: a failed reimbursement in production points at the world, and the world is cited.

Reviewed forWhich provider changes lack observed research and a citing constraint? Look at the provider facts the change relies on, beside the research records.

Marked guidance: a reviewer answers this question.

A regulation with a deadline needs working behavior before its requirement exists, so the constraint carries the rule in the meantime. The release stays shippable until the statutory date, and only then does the missing behavior block it. Without this path teams either ship late or build the rule where no record owns it.

Reviewed forWhich anticipatory behavior lacks a citing constraint, or blocks a release before the statutory date? Look at the regulation-driven Behavior records beside the constraint and its date.

Marked guidance: a reviewer answers this question.