Are you an LLM? Read llms.txt for a summary of the docs, or llms-full.txt for the full context.
Skip to content

AppGen

AppGen turns app intent into a formally-specified app. It abstracts ~1,500 reference apps into a generative model and produces validated enclave graphs, SDK code, and deployment artifacts for 11 platforms — but the AI never writes arbitrary code. It only selects from and composes a closed vocabulary of verified building blocks, so every generated app inherits the protocol's formal guarantees.

How it works

  1. Classify. A classifier maps the natural-language intent to an archetype — a known substrate app, team-chat, social-feed, or custom — as a closed-schema decision, not free text.
  2. Resolve parameters. For non-substrate archetypes, a resolver extracts typed parameters (workspace name, encryption mode, …) against the archetype's schema.
  3. Constraint-solve. A deterministic solver applies defaults, type-checks the parameters, and enforces constraint rules (e.g. "AI summary requires full search"), returning solved params or a structured correction list.
  4. Generate the manifest. The archetype's generator produces an app manifest — the RBAC matrix, event definitions, plugin-slot bindings, and encryption topology.
  5. Validate + translate. Structural checks and algebra tests (via the UI Kit) validate it; a translator converts the app spec into deterministic Lean that must compile.
  6. Platform codegen. The validated spec feeds CodeGen's fan-out to 11 platform targets — web, native, desktop, extension, CLI, TUI, Cloudflare Workers, embedded, and more. Each target gets the same logical app and semantics; only the bindings differ.

What makes it sound

The lever is the closed vocabulary: ~23 primitives arranged into ~31 canonical shapes (PublicFeed, Channel, ContentMarket, OwnerProfile, …), each instantiated as Lean theorems. The AI touches only classification and parameter binding; generation, validation, and translation are deterministic. So however the LLM arrived at the spec, the emitted Lean must compile and carry its proven properties — 25 in total (12 from the core guarantee matrix, 13 from substrate theorems, all sorry-free). When the model errs, it errs within the schema, where the solver and validator catch it; it cannot produce arbitrary code.

Figures

  • ~1,500 reference apps abstracted; ~31 shapes · ~23 primitives · 40+ archetypes
  • 25 proven properties (sorry-free Lean), across 11 platform targets
  • a deterministic (named-app) path resolves in ~90 ms; the AI-assisted path in ~1–3 s

See also