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

Introduction

CVN is the shape an application takes when its kernel cannot touch the world and its host cannot decide anything.

  • The kernel holds a Model and an update that is total and synchronous: every action returns a new model and a list of Cmds — data describing effects, never the effects themselves.
  • A host (node, web, native) performs Cmds through ports it declared, and hands the kernel the capabilities it cannot own: a clock, timers, storage, the network, randomness.
  • A declaration on the runtime says what the kernel owns, what it still borrows, and what the host must provide. The port is done when the borrowed list is empty — and the gates make sure "done" was not written by hand.
   action ──▶ kernel.update(model, msg) ──▶ [model', Cmd[]]
                                                  │
                                       dispatcher records, then drains
                                                  │
                                    host.performNow(cmd) ─▶ ports

What the shape buys

An effect that goes nowhere says so. A Cmd the host cannot route is reported — [cmd] not performed: no persist port — and the log gate fails the run. The alternative is the defect this whole shape exists to remove: a write that silently did not happen, behind a guard that asked a port whether it would work.

A decision is data, so a test can read it. { kind: 'submit', target: { to: 'enclave', id }, encrypt: { scheme: 'sent', to, text } } — which cipher seals a write is the kernel's decision and the host's execution, so the decision is assertable without a network, a key, or a browser.

The claim is measured, not written down. Every rule has a gate: declared ports equal supplied equal travelled; the kernel names no platform global; a conformance corpus replays through the shipping module and not a copy of it. A claim with no gate drifts within a week — measured, repeatedly.

Proven in Lean, replayed in TypeScript. The protocol rules and one app's own decisions are executable Lean with theorems checked by Lean's kernel. An oracle emits the corpus; the real code replays it. A model nothing replays is a proof about a path nobody takes.

A first look

import { createRuntime, router, performed } from '@enc-protocol/cvn'
import { createNodeHost } from '@enc-protocol/cvn/node'
 
const host = createNodeHost()
const rt = createRuntime({
  initial: { count: 0 },
  runAction: (cell, perform, path) => {
    if (path === '/inc') cell.commit({ count: cell.value.count + 1 })
    if (path === '/save') perform({ kind: 'persist', key: 'count', value: cell.value.count })
  },
  performNow: router({
    persist: (cmd) => (host.store.setJSON(cmd.key, cmd.value), performed()),
  }),
})
rt.action('/inc')
rt.action('/save')

Where it came from

CVN was extracted from impl-super-mvp — a running messenger — by moving the application runtime into this shape one borrowed method at a time, with every claim tied to code by a gate. Nothing here is a design sketch: it is what survived that, and The rules are stated in the order they were paid for.

What is in this package is what survived: the dispatcher, the state cell, the runtime, one host contract with node and web behind it, a conformance suite every host runs, the gates, and cvn/enc — the ENC rules the port surfaced, each pinned by a Lean model whose cases the real code replays.

Where to go next

  • Concepts — Model, Cmd, dispatcher, host, ports, declaration.
  • The rules — each one stated as it was learned, and what it cost.
  • Hosts — the contract, then node, web, native.
  • Gates — the checks that keep the shape from drifting back.
  • Formal spec — what is proved in Lean, and what replays it.
  • Porting an app — the six steps, and the traps.