What is proven (and what is not)

A framework that says "formally verified" without saying what is verified is worse than one that says nothing, because it transfers confidence it has not earned. This page is the boundary, stated so it can be checked.

Proven, by theorem

These hold for every app on the framework, discharged once at lake build and audited by test/axiom-audit.mjs against sorryAx and unexpected axioms.

Theorem	Module	Statement
`refines_sound`	`Encapp/Store.lean`	if a `World` refines the emulator under some relation, then for every command sequence the emitted event traces are equal and the final states stay related
`refines_log`	`Encapp/Store.lean`	corollary — a refining world ends with the same observable committed log
`reversedWorld_refines`	`Encapp/Adapter.lean`	a genuinely different representation (log stored reversed) does refine, so the refinement machinery is not vacuous
`applyEv_idem`	`Encapp/Replay.lean`	re-applying an event with a seen `id` is a no-op
`replayLog_append`	`Encapp/Replay.lean`	folding `l₁ ++ l₂` equals folding `l₂` after `l₁`
`App.ofMsgLog_append`	`Encapp/Core.lean`	reload equivalence at the abstract TEA layer
`store_ok`, `ui_over_store_ok`	`Encapp/Bridge.lean`	the append-log store refines the seq-counter spec, and the UI layer over it lifts by `Foundation.Layer.mono`
`Layer.mono`	`Foundation`	pinned to exactly zero axioms by the audit

Per-app, each workflow adds:

Theorem shape	Statement
`w.holds app = true` by `native_decide`	every `Doc` post-condition of workflow `w` holds after replaying its steps through the reflected interpreter
`corpus.all (·.holds app) = true`	the aggregate — the whole corpus in one decision
`corpus.all (·.users.length ≤ 1)`	the single-user emit is faithful to the proof semantics

native_decide proofs carry the Lean.ofReduceBool axiom. The audit pins that explicitly rather than letting it pass unnoticed.

Checked, but not proven

The JS runtime is not proven to equal the Lean interpreter

This is the most important gap, and the framework says so in its own source. Encapp/AppGen.lean describes the emitted runtime as "the operational mirror of reflStep … so the deployed app and the Lean semantics agree by construction (checked empirically against the emulator oracle)."

There is no Lean theorem relating appCoreJs to reflStep. What exists instead is empirical, and it is substantial:

the same corpus replays on four independent runtimes (happy-dom, headless Chromium, React-Native-web, real Electron) and every Doc post-condition is re-asserted there;
test/native-core-identity.mjs asserts the web and native cores are byte-identical, so a divergence would have to be a divergence from Lean on both platforms simultaneously;
test/fuzz-parity.mjs does seeded differential fuzzing of synthetic apps across web and native, with a curated regression set of seeds that each caught a distinct divergence class.

So: replay evidence is emitter-fidelity evidence. Treat "the proofs hold" and "the shipped JS does what the proofs say" as two claims, of which only the first is a theorem.

Crypto is axiomatized

Signatures, hashes, sparse Merkle trees and ZK are axiomatized. The proofs cover data-plane logic, not the cryptographic primitives.

Scoped, by design

The proof tier is single-`Doc`

reflRun has a single-Doc semantics, so a workflow proof is single-app-instance logic. Multi-user and cross-enclave stories are the node layer's concern. The emitted corpus still carries a users list so a multi-client runner can project it, but the native_decide theorem is about one instance. corpus_single_user makes that boundary explicit rather than leaving it implied.

The workflow framework covers `ReflApp` + `Doc` apps

Apps interpreted by reflRun (the flagship, hello) are in scope. The Spec / App Int examples such as Counter use a different state model and are out of scope for the workflow DSL without a rewrite.

The generality boundary

Encapp is often described as "protocol-free", and at the framework level that is exactly true: HostBinding requires only toJson, AppGen never inspects what a binding means, and no framework module imports a protocol.

It does not follow that any app UI can be built today, and the distinction matters:

The effect algebra carries chat vocabulary. postRow in Encapp/AppGen.lean hard-codes a message row — from, body (read from the draft scalar), media, trailing, outgoing. The constructors pushDraft, pushInput, setConvId, pushConvMessage, routeIfHex64 and lookupRoute are framework constructors, not app data.
There is a domain-free path. appendFromScalars and appendFromScalarsIfAbsent build a row from declared constants plus named scalars, with no chat assumptions. A non-messaging app uses those and avoids the chat constructors.
The evidence for domain-freedom is thin at the emitter level. Encapp/Examples/Counter.lean is a genuinely non-messaging proven app, but it uses the simpler Spec / App Int surface, not ReflApp + AppGen.emit. Hello.lean — the only other example — is messaging-shaped (pushDraft "messages"). No non-messaging app has yet gone through the full SPA pipeline.

The honest phrasing is therefore: the framework core is protocol-free; the SPA emitter's effect vocabulary is not yet domain-free. Shipping one non-messaging app through AppGen.emit is the single piece of evidence that would change that sentence.

The host adapter is hand-written

Encapp emits the app. It does not emit the host. A deployment supplies an adapter implementing the store seam, and that adapter is ordinary hand-written code outside the proof boundary. For the flagship app that adapter is roughly 2,400 lines of JavaScript.

This is the layer where defects concentrate, precisely because the proofs cannot see it. The mitigation is to move policy out of the adapter and into the app's declared binding, so that deleting a declaration makes a test go red — see Host bindings.

How to check any of this yourself

# every theorem, including each workflow's native_decide
~/.elan/bin/lake build
 
# axiom hygiene: fails on sorryAx or any unexpected axiom
node test/axiom-audit.mjs . Encapp.Examples.hello_reflected_matches Lean.ofReduceBool
 
# the keystone must have exactly zero axioms
node test/axiom-audit.mjs . Foundation.Basic Foundation.Layer.mono ''
 
# the whole gate: proofs, coverage, native parity, fuzz, replay
node test/hello-matrix.mjs

If a claim on this page cannot be refuted by a command, treat it as marketing and open an issue.