Current milestone — the v0 validator/transpiler (scope settled). v0 implements §3–§21 as written — plus two constructs adopted after the original scope statement (transient act, §4 "Transient acts", from the transient-acts investigation; the act's closure act ... with, §6 "Inline part creation"; deletion and its trigger family, §12 "Deletion" and §13 "Deletion as a second exit cause", from the delete investigation) — validated and transpiled to an executable runtime driven through a test-harness boundary, itself fully settled. Input enters through the act construct: each act declaration transpiles to a typed input value — a Kotlin data class of the act's stored fields, NewSubmitPayment for act SubmitPayment — and a commit overload that takes it: the thing the engineer's own transport code calls to submit a mutation, and a class any transport can bind a request to by reflection with nothing written by hand — plus a generated main-style entry point for driving the system manually. The declaration names no mechanism; transport, persistence, and serialization are the engineer's code, outside the spec (the external-input item below). A call returns acceptance or a refusal, each carrying the input value it was handed, so a refusal holds what was refused as the engineer's own type and never as a map; a refusal names what was violated — the type-level failure or the specific never, the latter carrying its context as data (§21) — and on refusal nothing commits. Refusal is whole: the unit accepted or refused is the closure the commit would have been (§4), never a part of it, so a request that should succeed in part is submitted as separate acts, or lands whole with its refused subset an ordinary refinement the rules answer (§2, the errors-are-refinements pattern; §4 "Every request gets a response"). Ticks enter the same way — each schedule name transpiles to a tick function the harness calls, since scheduled events and user acts are both external input (§4, §17) — so schedule definition is not needed; when that construct lands, it defines when the tick functions are called, never what they do. Reading is a query API the caller composes, over model objects: every shape and refinement has a generated data class, the model object, every field read once at the moment of the read; a model object is itself a reference to its record (Ref<Invoice>, one type for both sides of the store boundary — a store row carries the same thing for each to-one field), so it passes wherever a reference is taken, equal to any other reference to the same record — equality is identity, and comparing fields is how an engineer asks whether two reads differ; a reference field holds a Ref<T> and read(ref) resolves it; and a query over any shape or refinement is composed by the caller from the spec's declared vocabulary (properties, references and inverses, refinement membership, the predicate language of §10, a required order over orderable datums, a page), returning model objects. A store key fetches one instance by identity the same way. Nothing is read through a reference: a view with getters would be a second, live read path beside the snapshot, and there is one. The spec declares definitions, never a query: a question a screen asks is written by whoever asks it, checked against the spec, and is not a line in the spec (OQ51, 2026-10-12). Querying is "read" in §4's sense and commits nothing. Built: the read protocol and its engine (compiler/src/main/kotlin/velle/Read.kt — a query as a value, checked by the validator's own predicate rules, answered from a read-only snapshot, ordered with the store key as the hidden tie-break, paged by cursor, counted and summed), the generic entry beside commit on the runtime, and per spec the typed Kotlin builder (read.invoices.where { balance gt 0 }.orderBy { due.ascending }.page(20).fetch(), read(inv.customer), read.invoice(key)), one model object per shape and refinement (a static union is an interface its operands implement; a membership flag per refinement over the same base), and a registry for queries the engineer names (examples/billing/output/src/test/kotlin/velle/QueryApiTest.kt). Deferred past v0, with their items below: Mapping, schedule definition, the act construct's remaining details, the state partition declaration, extensible data types, and why/provenance — plus visible to ... where, removed from §10 until re-derived and synced. Nothing cut is exercised by any current example, and each re-enters post-v0 through its own item. The whole-language grammar is settled and normative in grammar.md — value expressions included, closing the formalization gap ## Predicate expressions once left open for derived-property formulas. The operational semantics and the validator's check catalog are settled and normative in evaluation.md and checks.md — the evaluation model an implementer follows (with its five signed v0 spike choices, the transient-act removal semantics, and the universal-transaction contract U1–U5 the engineer's store must honor) and the check catalog the validator runs, the coarse fail-closed slices of the open calibration questions included. The v0 implementation lives in this repo, split along the architecture's seam ("The extension framework," below): compiler/ holds the lexer/parser from grammar.md, the validator from checks.md, the runtime from evaluation.md, and the harness codegen; stores/sqlite/ holds a generic, model-driven store over SQLite — the framework role, implementing the runtime's store protocol once for every spec — that every example's tests run their flows over, in memory and then through storage; each example under examples/<system>/ pairs its spec with its own transpiled, developer-owned output/ module (gradle generate) and the tests that drive it — with examples/billing/billing.velle as the first spec, parsed, validated, executed, and exercised through its generated typed surface, and examples/membership/membership.velle as the second, written to exercise the surface area billing leaves untouched (optionals and narrowing, or-composition, the ledger with latest, flag-witness guards, episodes as data, sibling joins and as reach-backs, bare frozen, act-sourced captures, the reconciliation latch pair, tolerates), and examples/payments/payments.velle as the third — the first written business-outward — assembling the errors-are-refinements interaction pattern end-to-end (async processor verdicts as later external commits, outcome-state dispatch, retries under a cap, timeouts, compensation on exhaustion) plus the handled-once act partition, derived refinement-body properties, composite bodies with freezes, and duration addition, and examples/enrollment/enrollment.velle as the fourth, exercising §6's collection constructs end-to-end (a declared m2m many with its inferred inverse, many <scalar>, reference-set act fields, whole-set replacement, +/- union and removal, fan-out assignment, derived collection views, and the boundary's duplicate refusal), and examples/orders/orders.velle as the fifth, exercising §6's act closure end-to-end (act ... with with a nested level, the generated nested input types, language-populated back-references, per-part rule firings, the boundary refusal rolling back the whole closure, and the derived aggregate on the container), and examples/gallery/gallery.velle as the sixth, exercising cross-base unions (§6, §9): the polymorphic association, the inverse inferred onto every operand, a derived body on the union, a rule over a refinement of the union, per-operand narrowing in a value expression and in a never, and the boundary's type-level refusal of a reference outside the union, and examples/moderation/moderation.velle as the seventh, exercising deletion (§12, §13): delete as a rule effect, undeletable refusing as data, the absorbing reference reading as absent, the records a deletion leaves behind, and the deletion-side exit triggers, and examples/peptides/peptides.velle as the eighth — the first written against a whole domain rather than around one construct: a crop-protection discovery pipeline whose lab, greenhouse, and field stages each keep a time series (hour-marked assay readings, day-marked disease scores, a climate log, daily site weather, field scouting, harvest), exercising the predecessor recurrence over a business datum (a running peak; the area under a disease-progress curve), means as sum over count, windowed sweeps for a silent sensor and an overdue score, two series correlated by date arithmetic, stage gates as transient requests answered by records, a never at the boundary over a transient request, admin-scheduled collection tasks over a static union of the two trial shapes (done when every plot has data at the task's day mark, nagged daily while overdue, reschedulable and cancellable until done), and a series locked by undeletable and refused-as-data corrections once its trial is evaluated, and examples/pharmacy/pharmacy.velle as the ninth — the second domain-first spec, a retail pharmacy where customers, pharmacists, assistants, and administrators act on the same records: a prescriber's order arriving with its prescriptions as an act's closure whose part-level prohibitions refuse the whole order, a drug interaction found from either drug through an or-formula view over a two-field shape, an allergy matched by a sibling join over two declared many edge sets, a two-hop derived view on the patient, the actor on every act a person commits (by LicensedPharmacist as the licence gate in the header, by Staff as filledBy as the business name the fill reads, a hiring act gated on an administrator with the first one seeded outside the trust boundary, a durable act storing who recorded it), with the remaining role gates as refusals over the request reading the actor, a fill request answered three ways (refused with nothing kept, refused on record with a reason, or constrained on the fill it produces), a capture of the day a fill reached the counter read by the nightly return-to-stock sweep and again at exit, a when leaving rule naming only a schedule so that a prescription expiring by age is told apart from one used up or discontinued, a price ledger ordered by its effective date and read through today with a future-dated change deletable and one in force undeletable, a static union as a notice's recipient, stock on hand as a derivation over receipts, fills, returns, and cycle counts, and recalls, reorders, claims, and the monthly controlled-substance snapshot as sweeps. and examples/vendors/vendors.velle as the tenth, written for the read side of authorization (§8, "Who may see a record"; "The actor" below): a catalogue whose products are shown to the staff assigned to their vendor and to administrators, a cost and a margin shown to administrators alone, a public vendor, the spec-wide default, the generated viewer reads with their per-viewer interfaces, the engineer's unfiltered view, a refusal projected for the actor, and a margin calculated from a cost the viewer cannot see. What remains in the open-questions index is calibration that running realistic specs will answer.

• State change & rule mechanics — remaining frontier. The core is settled — assignment and one-writer (§12), deletion as a mutation whose legality is derived (§12 "Deletion") with its own exit cause (§13 "Deletion as a second exit cause"), run-once guards with no sugar (§18), folds and tolerates (§19), the pattern spectrum and rung recognition (§20), and "what is one commit": a commit is exactly one statically-shaped closure — one act instance in the common case, the container plus its declared inline parts otherwise (§4; §6 "Inline part creation") — a body is one commit, consequences share the act's transaction by default, after commit declares a boundary, and the irreducible world/state gap at an external effect is answered by the intent-before-effect pattern (§4, ## rule "Transactions and after commit"); commit timestamps are author-declared, language-populated fields (timestamp on create / on update, §5); every instance carries an opaque, readable id (§5); a rule fires once per matching record — no loop construct, transaction scope following the trigger source (§16, §17); all-or-nothing batches need no envelope construct — they dissolve into one-body effects, commit-shared fan-out, one-fact-many-readers, containers, and completeness gates (§20, "All-or-nothing batches"); cascades nest as trees of transactions; tolerates loss signs fire-and-forget external effects (§11, §19); and never declares impossible configurations — transaction-end enforced, proven for guarantees, compiled into the boundary for refusals and constraints (§21); and shapes are marked externally committable by act declarations — the trust boundary — with the construct's remaining details deferred ("External input," below; resolves OQ5); and an exit rule is the last reader of the leaving refinement's captures — retraction lands at the exit commit's close, full pre-state access is rejected, and capture-reading rules are transaction-bound (§13; resolves OQ7's exit-read thread, with its two remaining threads moved below). Still open: the order-independence/confluence and quiescence proofs (OQ16). Refusal is settled: it is compiled boundary code from never (§21), whole and pre-commit (the scope statement above); who may commit an act is a prohibition reading the actor the act's by clause binds ("The actor" below), and authenticating that person is engineer wrapper code ("External input" below). Ordered folds and firing order at a tick was OQ15, settled: rules carry no ordering clause — the predecessor recurrence is the served spelling (§19), and growing its certificate whitelist folded into OQ16's calibration as one shared vocabulary. Whether the canonical guard form is pleasant enough to be what fold diagnostics ask authors to write was OQ14, settled: it is — the canonical form stands as the diagnostics' fix-it spelling, no sugar added (§18).
• Mapping (shape-to-shape translation, e.g. API DTO → domain shape) — part of the original design goals, not yet exercised in a worked example. Now also the natural home for a direct per-member effect spelling — "one Reservation per line item" — as sugar over the guard-correlated fan-out (## State-change patterns, "All-or-nothing batches"), whose inverted spelling gets unpleasant as correlation deepens.
• Schedule definition — on Daily (the header's on clause) settles how a rule references a schedule; what actually defines Daily (cadence, timezone, one-off vs. recurring) is a separate, not-yet-designed construct, assumed to be a cron-like scheduling framework.
• Latency vocabulary — on expresses the evaluation source, not latency requirements. Whether "immediate by default, named schedule otherwise" suffices, or deadlines ("within 24h") deserve first-class expression the compiler validates against declared cadences, is undecided. (Moved here from OQ7 at its resolution.)
• on commit of <Shape> narrowing — "only withdrawals suspend, not fee assessments." Expressible and occasionally meaningful, but it can silently miss entry paths; per flexible-not-restrictive it would be allowed with the compiler reporting exactly which entry paths go unobserved. Not yet designed. (Moved here from OQ7 at its resolution.)
• External input (act) — resolves OQ5, "marking a shape as external input." Velle implements no transport: REST APIs, GraphQL, socket connections to a message bus are traditional-code territory it doesn't compete in; what it owns is the contract between the spec and the shape of the transpiled code. The construct names no mechanism (it originally carried a using <Mechanism> clause over transpilation plugins, dropped when the runtime model settled): transpilation generates one typed input value and one commit overload per act — the thing the engineer's own transport code calls to submit a mutation — and mapping any transport onto those input values is the engineer's code, permanently, not a deferred plugin design. An act is declared in exactly one place, where its fields are (act CorrectEmail { ... }): the keyword is the shape declaration plus the boundary, not the act-level sugar §12 rejects — nothing is hidden and no positional invariant is spent — and there is no second statement that opens a shape declared elsewhere (OQ50, settled 2026-10-12). An act is externally committable; a shape enters state only as a rule's effect. The set of act declarations is the trust boundary: the never guardrails for refusals and constraints (§21) compile to the generated surface at each act's boundary, and reachability sharpens — a shape with no producing rule is uncommittable, so a rule triggered by it is the unfireable-rule error (§11). Authenticating the caller, finding their record, rate limits, quotas, and which machine clients may call which endpoint live in the engineer's wrapper code before the commit call, outside the language; who may commit an act, and who may see a record, is the spec's, through the actor ("The actor," below; OQ33, settled 2026-10-15). Which fields the committer supplies is read off the declaration forms — there is no field policy to state (resolves OQ31); a closure declaration (act ... with, §6 "Inline part creation") extends the same reading to inline parts, each a nested input value carrying every stored field minus the language-populated back-reference. The generated input value carries every stored field of the act: the committer supplies them all, an optional (?) field by explicitly supplying the absence, and a convenience default belongs in the engineer's wrapper before the commit call, with the transport mapping it already owns. Derived properties are legal on an act and are never fields of the input — nothing is stored, so there is nothing to supply, and the = expression form states in the language that the value is calculated (on a transient act, whose one evaluation moment is its own commit, a derived property is also how an arrival-time value is fixed). initially and timestamp declarations on an act are compile errors (checks.md V21): a system-maintained value is no part of an external submission, so it lives on a shape — supplied by a materializing rule's from block, minted by initially at that record's creation commit, or populated as timestamp commit metadata — with the transient-act materialization (§4) as the served spelling for a request whose durable record carries such fields. Still deferred as details of the construct, not open language questions: supplied-vs-generated id at a trust/legacy boundary (a legacy table's primary key, an upstream system's reference — mapping-side mechanics ride with the Mapping item, above). act is strictly input (OQ51, 2026-10-12): reading never goes through an act.
• The actor (by) — resolves OQ33, authorization (settled with Dave 2026-10-14 and 2026-10-15; built 2026-10-15 for the stored actor, compiler/src/test/kotlin/velle/ActorTest.kt, examples/pharmacy/pharmacy.velle). An act a person commits says so in its header: act LicenceRenewal by Administrator { ... }, transient act FillPrescription by Staff as filledBy { ... }. The shape after by is a shape, a static union of shapes, or a refinement of one — never an act, since an act is an input and the person who commits one is a record; a refinement there is the role gate in the header, one desugaring to LicenceRenewal requires actor to be Administrator, which stays legal to write in the body beside it (a two-role gate, SetReorderPoint requires actor to be Administrator or actor to be Pharmacist, is written that way or over a composed refinement). The clause binds the committer in the act's scope under the name actor unless as chooses another; nothing is reserved, actor is an ordinary identifier wherever no clause binds it, and a scope that declares a field under the bound name is told to name the actor (checks.md F3). The actor is a fact of the commit in the family of id and timestamp (§5): never in the generated input value, never claimed by the committer, never assigned, and on a durable act stored under the bound name with nothing declared, readable through any reference to the act (renewal.actor) for as long as the record exists, so an after commit or scheduled rule over the act reads it on every firing path alike — the memory is data, and the tick law (§17) is untouched. An act without the clause has no actor: a processor's verdict or an insurer's adjudication arrives from a machine and says nothing. The generated commit function of an act declared by takes the actor as a parameter beside the input (commit(NewVerifyFill(...), pharmacist), a Ref to the base shape), and the binding hands it the record it resolved the authenticated identity to — one resolver registered once, the shape of Spring's filter rather than JAAS's per-call lookup; a missing actor, or one of the wrong base shape, is a type-level refusal, and one outside the named refinement is the requirement's refusal with the actor's record in its rejection data (§21). Where actor may be read is where the compiler can prove which act is in scope: the act's own prohibitions, refinements, and derived properties; any rule whose subject is the act or a refinement of it, at any cadence; and an on commit rule whose subject is a product of the transaction, which declares what it reads in its header (rule LogQuarantine when Quarantine by Staff? { ... }) and is typed by reachability over the condition graph (checks.md V31): by Staff when every path to the trigger starts at an act declared by, by Staff? when some path starts at a tick, an after commit firing, or an act without by, where the actor is absent and the body narrows with actor is some as it narrows any optional — "the user if there was one, or system" is if actor is some then actor.name else "system", with nothing reserved for the system. There is no system identity: a spec that wants a job to commit a gated act models the job's actor as business data (a staff member with a system role) and the binding provides it as it provides a person; and a tick has no actor. Bootstrapping is not the language's problem: the first administrator of a system whose hiring act is gated on an administrator is seeded by the engineer outside the trust boundary, as a migration or fixture row is — VelleSystem.seed is the in-memory form, no door, no rule, no prohibition (evaluation.md, "An exposed call"). The read side is the same person seen from the other direction (§8, "Who may see a record"; built 2026-10-15, compiler/src/test/kotlin/velle/VisibilityTest.kt, examples/vendors/vendors.velle): visible to <Shape> [as name] [where ...] as a body clause on a shape and after a field's type, visible to anyone for a public one, several clauses disjoining, a shape's own replacing the spec-wide default written once at the top; required on every readable shape once a spec has any by or visible to (checks.md V32); applied by the read surface only — read(viewer) on the generated system takes a reference to any shape a clause names and returns the same roots with every query carrying the viewer, every fetch resolving absent for a record the clauses do not admit, and every model object projected: one class per shape declaring each field once, a gated field nullable in it, and one interface per viewer shape per shape with gated fields listing what that viewer may see, so a screen written for staff cannot compile against a cost it may not have; the engineer's own read stays the unfiltered class, their view of their own store — and never inside evaluation, so a derived property is calculated from every input whoever asks (§7). A refusal is handed back through the same surface: its rejection data is projected for the actor as a read would be, the act they committed whole and the records it read through without the fields they may not see. An actor built from an identity provider's claims rather than stored (transient shape Staff) is the remaining slice: designed (an unstored shape the resolver builds per call, correlated to stored records by a business key, V17 restated so nothing stored references it), built by nothing yet, and listed in QUESTIONS.md. Reference §8's rule stands with one step taken: a transaction has an actor and actor names it; what §8 still excludes is a user who exists outside any act.
• Reversal — resolved as a non-issue for the language itself: it's a business-policy choice, expressed via which artifact shapes a human declares. Two candidate idioms exist — the resolution artifact (now exercised as membership's delinquency episodes) and the grace-period suppression window (unexercised) — but no single canonical pattern has been adopted.
• Escape hatch / override syntax — how a human marks part of a spec as intentionally hand-implemented/AI-implemented rather than declarative. Deferred; agreed to be a lesser concern until the core language settles.
• Compiled guardrails — the idea that the compiler/transpiler should structurally enforce best practices (e.g. forced prepared statements, automatic error-context capture, correctly evaluating self-referential shape/derived-property definitions, how deep narrowing analysis for .-vs-?. sees through nested expressions, erroring — not silently resolving — a bare unqualified name that doesn't exist in its innermost scope but would resolve unambiguously in exactly one enclosing scope, per ## Principles's compiling-as-validation rule: the fix is always an explicit this.field, never an inferred scope-walk that could silently start pointing elsewhere the moment an enclosing shape gains a same-named field; a field addition that creates a new type-match ambiguity for an existing bare for reference elsewhere in the spec, per §14, must be reported as one connected diagnostic naming both the declaration that introduced the ambiguity — e.g. Referral gaining a second Customer-typed field — and every reference it now makes ambiguous — e.g. CustomerWhoReferred's for this — since the compiler's job is reporting an incoherence in the spec as a whole, not a syntax error in one isolated line, and a human should never have to search for why an untouched line stopped compiling) as a byproduct of codegen. A design principle, not yet a syntax construct — with one member now sourced by syntax: runtime boundary validation derived from the refusals and constraints never declares (§21).
• Extensible data types — author-declared scalar types beyond the builtin list (## Scalars). Money is the canonical example, demoted from builtin when the scalar list was pinned to Kotlin-grounded types: currency, precision, and literal syntax are exactly the kind of domain judgment an author should declare, not a builtin should assume. What declaring one means — underlying representation, permitted operations, how sum and comparisons extend to it — is undesigned. The examples keep using Money as a preview of the capability. One citizen of the extension framework, below.
• The extension framework — custom data types (above) and custom predicate/value functions are one concept wearing two hats: registered extensions — traditional code the developer hands the compiler at execution time through a registration API. Three commitments shape the design. Registration carries validator-facing metadata: an extension declares what the checks need to know about it — a custom function's algebraic properties (idempotence, duplication/reordering insensitivity: the ## Self-referential folds whitelist generalized from a builtin table to a registration contract), a custom type's permitted operations and orderability — so the closed builtin list (## Scalars) becomes the registered list, and the validator typechecks calls and discharges fold hazards against the registry rather than a hardcoded set. Extensions are distributable: workspace-local custom code the compiler locates, or packaged, installable libraries — shared business-domain extensions (a "Velle finance extensions" library carrying Money, its operations, its literals) — the same artifact either way. Extensions are not output: the transpiled code lives in the developer's workspace and the developer owns it, while extensions live separately, because they change on different axes — a spec edit regenerates output but never touches extensions; an extension upgrade re-runs validation but never rewrites the spec. The resulting architecture has three parts: (1) the language + compiler/validator + environment, which locates extensions in the workspace; (2) the extension framework — types, functions, custom or packaged; (3) the transpile output — the developer-owned executable runtime, generated executable tests that verify the runtime against the spec, and opt-in derived diagrams (diagrams.md).
• initially generator vocabulary — randomUUID is the only generator so far (## Scalars); whether others belong, and which, is undecided. Sequence-flavored generators stay excluded on principle — ordering comes from timestamps or declared fields, never minted values.
• Exit from act-entered refinements — a membership predicate of the form exists ArchiveRequest for this is monotone: facts persist, so nothing can ever leave ArchivedInvoice, and un-archiving is inexpressible. Exit requires either pairing occurrences in the predicate — the simple unordered pairing (exists Receipt for this and not exists ReceiptVoid for this) is expressible today and is how a frozen state thaws (§8, "Frozen fields"), while ... and not exists Unarchival newer than the matched request, needed the moment re-archival enters the model, requires occurrence-comparison vocabulary not yet designed (its ordering source is settled — the occurrence shape's declared creation timestamp, or an author-named field — but the comparison/scoping spelling isn't) — or a mutable field the predicate reads. Both are expressible; which is idiomatic is unsettled.
• State partition declaration — refinement properties give states their data (## Refinements), frozen gives states their write permissions (## Refinements, "Frozen fields"), and reified acts give transitions their payloads — but nothing yet asserts that a set of refinements partitions a shape: mutually exclusive, jointly exhaustive ("an invoice is always in exactly one of Draft, Issued, Paid, Voided"). Candidate spelling states of Invoice = Draft | Issued | Paid | Voided, invoking the exhaustiveness/overlap check ## Refinements already names as a compiler goal — and the natural long-term home for per-state write permissions beside legal transitions (where "this field is frozen in every state" becomes the never-writable diagnostic). never (§21) is its natural primitive: pairwise disjointness is never (A and B), leaving only the coverage check. The next investigation.
• Spec-carried examples (example) — a future construct letting the spec itself declare named example instances, so generated executable specs (testgen.md) derive their scenario data from the description instead of demanding human-written givens — the description becomes self-illustrating, collapsing the given/derived split's human tier. Not yet designed; testgen.md phase 3.
• why / provenance — a command to trace which rule/refinement produced a given piece of state, mapped back to Velle source. Agreed as a goal; no syntax proposed yet.