Case study: Super

impl-super-encapp is the largest app built on Encapp: a Telegram-shaped multi-enclave chat client with DMs, groups and a personal moments feed. It is the app that has driven most of the framework's vocabulary, and the honest place to see both what Encapp buys and what it does not.

By the numbers

The last row is the important one. Encapp emits the app; it does not emit the host.

Shape

Super/
  App.lean        state, pages, handlers, gates, and the SdkBinding declaration
  Screens.lean    every screen as RView data
  Kit.lean        design-system helpers over ViewDsl
  Dm.lean         the DM sub-app
  Theme.lean      design tokens
  Workflow.lean   the corpus + corpus_all_hold + corpus_single_user
  Verified.lean   additional app-level theorems

Everything a user sees is emitted from these files. There are no hand-written .tsx / .jsx screens — a check in the app's own test suite fails if one appears.

What the proofs cover

theorem corpus_all_hold :
    allWorkflows.all (·.holds Super.App.app) = true := by native_decide
 
theorem corpus_single_user :
    allWorkflows.all (fun w => decide (w.users.length ≤ 1)) = true := by native_decide

54 user stories — create a group, kick a member, delete a message, accept a request, post a moment, reveal a private key, walk browser history — each reduced to a decision about the resulting Doc, all discharged in one theorem at build time.

The same corpus is then replayed against real infrastructure, which is a different claim: 52/52 workflows pass against spawned local nodes, plus multi-user DM and group flows driven in two real browsers.

The host binding, and why it grew

Super declares its store seams as data:

structure SdkBinding where
  package    : String
  cls        : String
  submits    : List (String × String)
  queries    : List (String × String)
  deletes    : List OpBinding
  moves      : List MoveBinding
  provisions : List ProvisionBinding
  peerSends  : List PeerSendBinding
  rowSubmits : List RowSubmitBinding
  peerRecvs  : List PeerRecvBinding

Each form was added for the same reason: a defect had lived in hand-written adapter code where no proof and no probe could contradict it.

• deletes — deleting a message was a hard-coded table comparison in the host. Declaring the op-dispatch made it reviewable, and removing the declaration now breaks a live probe.
• moves — leave and kick are membership transitions. Declaring from/to/subject/scope turned "which enclave does a kick target?" from an invisible convention into app data. Getting that wrong once meant kicking a member of one group on another group's enclave — a silent wrong-target write.
• provisions — "one enclave per group", the property that keeps a user's groups cryptographically separate, had been an unstated convention inside a role comparison.
• peerSends / peerRecvs — an invite is not one message. impl-super clients poll a Personal notice; Encapp's own peers send a DM invite. Sending or listening on only one rail makes the two implementations invisible to each other in that direction, which is precisely the bug that shipped. Both rail sets are now app data.
• rowSubmits — the profile payload is shaped from the row plus the caller's identity, which the generic submits list cannot express. It had therefore been written out three separate times in the host: the live seam, the pre-protocol flush, and the restore read — one app fact in three places, which is how two of them silently drift.

The rule that emerged, the hard way, is in Host bindings: declaring a rule is worth nothing unless the host reads it. An audit of this app found three declared fields that no host code consumed — deleting or flipping them changed nothing, while the project's own ledger cited them as evidence.

The claims ledger

Super carries a CLAIMS.md in which every assertion about the repository has a command that would refute it, checked by test/claims-check.mjs:

### the app's seams are DECLARED, not hard-coded in the host
- status: VERIFIED
- verify: sh -c 'grep -q "\"deletes\":\[{" dist/index.html && …'

A claim with no verify command is not a claim. A claim marked BLOCKED whose verify command succeeds fails the build, which mechanises the stale-rationale trap — a note asserting something is impossible must carry a command that re-attempts it.

This is not part of Encapp, but it is the discipline that made the framework's boundaries legible, and it is worth copying.

What Encapp did and did not solve

Solved. Every screen and every handler is proven data. A logic change cannot diverge across web, native and desktop, because there is one logic artifact. 54 user stories fail the build rather than a test run. Adding a screen is adding data, and the coverage gates refuse to let it ship untested.

Not solved. The 2,494-line host adapter is ordinary hand-written JavaScript outside the proof boundary, and it is where essentially every defect in the project has lived: an invite that travelled one carrier rail instead of two, a delete seam that silently no-opped, a leave that did not stick, four async calls whose failures were invisible. None of those were app-logic bugs, and none of them could have been caught by a proof about the app.

That is the honest shape of the guarantee. Encapp makes the app provable and the host declarable — it does not make the host disappear. The ongoing work on Super is moving policy out of the adapter and into the binding, one form at a time, with a deletion test for each. Eight forms have landed that way. Of the tables the app still touches through hand-written host code, auth_requests (wallet connect), lookup_requests (registry resolution) and session_ops (sign-out) are host by design — I/O and session plumbing, not app policy, and declaring them would push host mechanics into the app, which is the wrong direction.

Reading the source

impl-super-encapp lives beside impl-encapp. Start at Super/App.lean — the state, the page table, the gates and the binding are all in the first 400 lines — then Super/Workflow.lean to see how 54 stories become one theorem.