Genesis

2. The Computational Problem

2.1 The lost acknowledgment

The problem that anchors the program is old and simple. A long-running workflow sends a request to an outside system (a payment processor, a carrier, another service) and is interrupted before the reply arrives. After restart, its local record is consistent with two different worlds: the action never happened, or it happened and only the acknowledgment was lost. Retrying in the second world duplicates the effect. Declining to retry in the first loses the work. No amount of local logging distinguishes them.

2.2 The separation problem

Conventional stacks divide the surrounding questions among separate subsystems. A compiler or interpreter reads the program; a runtime executes it; an authorization layer decides what it may touch; a storage engine persists its state; a recovery mechanism restores it; an audit trail records what happened. Each part is usually correct on its own terms. The difficulty is at the seams. Whether a recovered program may still exercise a permission it held before the crash, whether two checkpoints are interchangeable for resuming but not for auditing, whether a cached result was computed under the authority of the call now reusing it: each of these spans at least two subsystems, and in most stacks no single component owns the answer.

The separation has three costs that motivated Genesis. Work is duplicated because each subsystem reconstructs facts the others already hold. State is represented inconsistently because each subsystem keeps its own notion of "the same state". And recovery is ambiguous because the conditions under which it is correct (what the receiver guarantees, what an acknowledgment means, how long deduplication keys are retained) are usually assumed rather than written down.

None of these observations is new, and Genesis does not claim to have discovered them. Its contribution, if it has one, is to treat them as a single design problem and to test which parts of a joint treatment survive contact with counterexamples.

3. How the Question Narrowed

The early phases of the program were adversarial by design, and most of the attractive ideas did not survive them. Seven hand-worked counterexamples removed claims that had seemed natural, among them that provenance edges explain results, that local contracts compose, that a durable intent settles an external effect, that compensation inverts an effect, and that recursive or "fractal" interfaces confer an advantage of their own. Section 10 lists them with what each changed.

An architecture tournament then compared five candidate calculi for a unified semantics: an evidence-preserving transformation calculus, a causal-continuity calculus, a composable kernel, a multiscale calculus, and invariant-guided recovery. It declared no empirical winner. It ranked the evidence-preserving calculus as the strongest single-calculus hypothesis and the composable kernel as the strongest multi-calculus one, and labeled both as hypotheses.

Two further lines were bounded rather than abandoned. A portable artifact format was found to presuppose an unavoidable shared bootstrap kernel, and bounded component synthesis was found to be exact only within a stated catalog and depth. What remained after these reductions is what the rest of this paper describes: an observation frame (§4), observation-relative summaries (§5), an authority algebra (§6), a work-elimination technique (§7 to §9), and a restricted toolchain that implements part of this (§11).

4. The Observation Frame

The observation frame is the research program's basic definition. It fixes a program P, an environment contract A, and a set of actors. A configuration is a six-part state

consisting of actor control q, volatile memory M, durable internal memory D, external-system state X (possibly unobservable), a durable outbox O of intents and receipts, and the set K of obligations and assumptions currently relied upon. A crash erases volatile state and keeps only what A declares durable. That is an assumption about the environment, not a property of disks, and the frame says so.

An observation of a run r is a six-tuple

of returned values, durable state, externally confirmed effects, failure and recovery status, unresolved effect intents, and observable happens-before constraints. The component u is the point of the frame. It records an effect not as done or not done but as a set of possible external outcomes, for example {not applied, applied}. The observer's knowledge set K_A(r) is the set of observations consistent with the durable evidence, and a statement that an effect did not occur is valid only if every member of that set excludes it. This is epistemic uncertainty, not probability.

The frame also separates modes of explanation, because they can disagree. In y := x OR w with x = w = 1, a dependency path runs from x to y, yet intervening on x does not change y, while x = 1 is still sufficient for y = 1. Structural reachability, counterfactual dependence and sufficiency are different questions, and an explanation must say which it answers.

5. Exact Summaries Depend on the Observer

5.1 When a state can be summarized exactly

Every optimization that skips work replaces a full state with a summary. The question is when the summary loses nothing that matters. Two short results, both standard and neither presented as new, give the discipline Genesis uses.

These are facts about quotients of transition systems, closely related to completeness in abstract interpretation and to bisimulation minimization. Their role in Genesis is a discipline rather than a discovery: a summary is never "the" compression of a state, only the compression for a declared observer and a declared set of actions. The instructive case is a summary that keeps only an account balance. It merges a state with a pending, uncertain charge and a state without one, and a retry then tells them apart.

Figure 3 shows the idea with two short histories. They end in the same recoverable state, so a summary made for recovery may merge them. They are not the same record of what happened, so a summary made for audit must keep them apart.

5.2 Finite checks

The research tested this on three finite automata, using two independently coded algorithms (forward partition refinement and backward pair-distinguishability) that agree on every class, not only on class counts, plus a direct pairwise check of each proposed class.

The exact-value row is the one that matters in practice. Two states with the same current balance but durable values 0 and 2 become distinguishable after a crash, so no representation can merge them while promising an exact post-crash balance. The implementations are controls on a known idea and are not competitive minimizers.

5.3 Exact composition

For a two-component model, local commutation squares plus one checked boundary rule prove by induction over interleavings that the product of two component summaries is exact. The decomposed check performs 614 comparisons (224 + 70 + 320) against 4,800 for a flat check, and two independent minimizers both find 160 global classes, so the product is the coarsest exact summary for that model and question.

The 614 figure isolates one proof obligation and is not total verification cost. A conventional assume-guarantee verifier with the same ownership and interface could use the same decomposition. What the experiment shows is that exactness can be checked compositionally when the boundary is stated, not that Genesis is required to do so.

6. The Algebra of Authority

6.1 Four states and four operations

Genesis models each permit, a delegable right to perform one action, as being in one of four states, encoded as two polarity coordinates (active, local):

Four operations move a permit only toward less authority, never back: τ_del takes Live to Delegated; τ_con takes Live or Delegated to Consumed; τ_aban takes Live or Delegated to Abandoned; and τ_del→con takes only Delegated to Consumed. Each leaves every other state unchanged. In the research implementation, a 64-bit bitboard reproduced the four-way partition of permits at each of the 45 steps of the test workflow's execution trace.

6.2 Seven distinct transformation maps

Applying the four operations in every possible sequence produces exactly seven distinct transformation maps on the four states, counting the identity (applying no operation). The research record contradicted itself here: its specification and report described a "five-element" algebra, while its raw result file recorded seven. Enumerating every composition of the five starting maps (the identity and the four operations), using only the operator definitions in the source code, gives seven. The five starting maps are pairwise distinct, and composition adds exactly two more. The figure "five" counted the starting maps. Because the seven maps are closed under composition and include the identity, they form what mathematicians call a monoid; nothing below depends on that name.

6.3 Why authority cannot be resurrected

The count of seven is a bookkeeping correction. The more useful result is a structural one, which the research record did not state explicitly. Order the four states by how much authority they retain: Live above Delegated, Delegated above both Consumed and Abandoned, with Consumed and Abandoned incomparable.

Two further properties, checked by enumeration, matter for anyone building on the algebra. The set of maps is not commutative: abandoning after delegating-to-consume differs from the reverse order, so the order in which a recovery procedure applies authority operations is part of its meaning. And not every map is idempotent: element 6 applied twice sends Live to Consumed rather than to Delegated, so "apply the same cleanup again" is not automatically harmless. Idempotence of τ_con and τ_aban individually holds, as a property of their definitions rather than a discovery.

The scope of these statements is the finite four-state model as defined, with its seven maps. They say nothing about a richer authority model, and they are statements about the algebra, not proofs that every path through the Genesis implementation applies only these operations; the latter is what the independent review in §11 tested, within its scope.

7. Case Study: Exact Crash-Cut Work Elimination

This section reports the program's most concrete computational result. It is one case study of the central question in §1, not a definition of what Genesis is, and a separate technical paper is planned to treat it at full length (§15.3).

7.1 The task

A bundling check asks whether two programs are observationally equivalent under every combination of branch decisions and every point at which execution might be interrupted. The test case compares package A, a sixteen-permit workflow whose four binary branch decisions form a tree, against package B, a single-coordinator, 44-step variant of it. With B = 4 branch variables there are 2⁴ = 16 branch assignments. Each execution contains 17 attempt steps, and an interruption can occur after any of the first M = 16 of them or not at all, giving M + 1 = 17 interruption points ("crash cuts") per branch assignment. The number of cases to compare is

7.2 The counts, reconciled

The research record used two numbers, 546 and 272, as if they were interchangeable. They count different things. Instrumenting the interpreter entry point and running both verifiers confirms the accounting below.

Figure 6 shows the mechanism. The table that follows reconciles the counts.

In general terms, comparing two packages directly costs 2·2^B(M + 1) interpreter runs plus any probes, and the projection approach costs 2·2^B. The saving is the factor (M + 1) in runs, paid for by the cost of computing and comparing projections. The 17.06× figure is a ratio of call counts. It is not a wall-clock speedup, and §9 shows that the wall-clock effect is smaller.

7.3 The projection, and when it is exact

Let T(P, b) be the single complete run of package P under branch assignment b, with no interruption, and let i₀ < i₁ < … be the step indices of its attempt steps. Instead of executing the interrupted run for crash cut c, the optimized verifier reconstructs the record that the interrupted run would produce from the complete run's record up to step i_c. Write that reconstruction Π_c(T(P, b)).

The proposition is deliberately modest. Its premises carry the content, and the research code encodes premise (d) with rules specific to the test packages: the set of unresolved intents is rebuilt by parsing attempt-label prefixes, and the candidate result is read from the first ledger step that introduces it. The experiment is therefore an executable check that the premises hold for two concrete packages, not a proof for the interpreter in general.

The check. For each of the 16 branch assignments and 17 crash cuts, the projection was compared field by field with a brute-force interrupted execution. All 272 comparisons matched on package A (reported by the developer) and all 272 matched on package B (editorial re-check, zero mismatches or errors on either). Package B matters because the equivalence verdict compares the two packages' projections to each other; exactness on one side only would not justify the verdict.

The control. A mutation replaced one call in a region reached only on an untaken branch. The optimized verifier rejected the mutated package with an observational mismatch. The baseline verifier's rejection of the same class of mutation is one of the gates the independent review exercised (§11).

7.4 What the comparison does and does not exercise

• One compared field is inert. A field that tallies outside-system boundaries by category is copied from the complete run to every cut. Across all 272 brute-force runs it takes a single value, so its equality check cannot discriminate between cuts or packages. The discriminating fields are the result, the unresolved intents, the consumed set, the live-or-delegated set, and the attempt labels.
• The fixture is symmetric in length. All 16 complete runs are 45 steps long. Branch choice changes which calls occur, not how many steps run. An asymmetric fixture has not been tested.
• One configuration. B = 4 and M = 16 only. No scaling claim is made.
• No concurrency or external drift. Both verifiers are deterministic, single-process, and use a fixed scenario. No concurrency, source drift, or unrecorded external effect is modeled.

8. Measured Quotients and an Incremental Cache

8.1 Observation contracts over the 272 records

The same 272 records can be summarized at different levels, each corresponding to a different observation contract (§5). The research specified seven levels and measured five. The two unmeasured levels have predicted counts in the specification; those predictions are not results and are not reported here.

Why Q5 is 21 and not 17. The research report stated 17 and the raw result file stated 21. The code defines Q5 as pairs of (result, number of unresolved intents). Recomputing from the code gives 21: three result values occur, with 1, 4 and 16 distinct counts respectively. The number 17 is a different quantity, the count of distinct unresolved-intent numbers alone, and a third reasonable definition, (result, the set of unresolved intents), gives 34. Because the class count depends on the definition, the only correct statement is the definition together with its count. This is the observation-contract principle of §5 appearing in the project's own bookkeeping.

Storage. The 272 brute-force records total 5,613,593 bytes as canonical JSON (about 20.6 KB each) and 698,716 bytes after general-purpose compression (about 2.6 KB each, a ratio of about 8). This measures ordinary compression of serialized records. It is not the storage cost of any quotient representation, and the class counts above are not storage figures.

8.2 An incremental verification cache

A second experiment memoizes verification work on content identity: each module's analysis is keyed on its name, a hash of its bytes, and a hash of the toolchain; each package-level specification on hashes of its source, its policy and the toolchain. On a six-module package, a cold check analyzed all six modules; an edit to one leaf module re-analyzed one and reused five; a comment-only edit reused the package specification; injecting a forbidden flow from high-security to public data invalidated the package entry and failed closed; and changing the toolchain version invalidated the specification cache.

This is a bounded test of invalidation over four kinds of change, not a proof that every incremental invalidation is sound, and it is a developer result from the post-preview research line, not a feature of the independently reviewed preview.

9. The Conventional Comparison

A result measured only against a project's own earlier baseline can reflect a weak baseline as much as a strong idea. The research therefore timed five variants of one verification-and-bundling workload on the same host. The recorded figures follow, with the conditions under which they were taken.

9.1 What the numbers support

• The projection removes most of the time. Optimized Genesis ran about 4.49 times faster than the preview baseline and about 3.07 times faster than the cache-only variant. The second ratio isolates the projection within this fixture; the first mixes projection, caching and avoided re-parsing.
• The saving belongs to the idea, not the language. The equally optimized conventional variant, which calls the same projection routine, reached 255.83 ms against Genesis's 239.20 ms, a ratio of about 1.07, and used less peak memory (1,714 against 1,895 KiB). Applying the projection to the conventional implementation improved it about 3.36-fold.

This is the expected outcome for an algorithmic saving, and it is the reason this paper calls the result exact work elimination rather than a Genesis speedup. Because variant 4 shares the projection routine, it is an algorithm-matched overhead check, not an independently engineered best-in-class verifier. The case for Genesis therefore cannot rest on speed. If it rests anywhere, it rests on whether stating the preconditions of §7.3 explicitly, as Genesis does, makes such optimizations safer to apply and easier to check. That claim is not tested by this benchmark.

9.2 Three quantities that should not be confused

This paper reports three different kinds of cost, and they support different conclusions.

• Interpreter calls eliminated. The bundling check needs 32 interpreter runs instead of 546 (§7). This is an exact, deterministic count on two fixtures. It measures how much execution was avoided, not how long anything took.
• Verification latency. The time to complete that check, measured in the five-way benchmark above. It fell about 4.49-fold against the preview baseline, but an equally optimized conventional implementation using the same projection was within about 7 percent, with no variance reported.
• Recovery latency. The time to recover an interrupted run. This paper reports no measurement of it. The projection result concerns verification, not recovery, and RC8's recovery command is defective (§11.5), so no recovery timing from it would be meaningful.

None of the three supports a claim that Genesis outperforms an equally optimized conventional implementation, and this paper makes no such claim.

9.3 What the numbers do not support

• Absolute times are inflated by the measurement. The benchmark ran Python's allocation tracer throughout the timed loop. Timing the two standalone verifiers with and without it on the editor's host (two runs, ten timed calls per cell after a warm-up) gave about 100 to 133 ms for the baseline and about 30 ms for the projection without tracing, and about 650 to 1,014 ms and 184 to 228 ms with it: an inflation of roughly six- to eightfold. The baseline-to-projection ratio stayed between about 3.3 and 4.5 in every run, with and without tracing.
• Five iterations, warm caches. Each variant ran five times; caches were cold on the first iteration only, and the mean averages cold and warm runs together. The figures are neither cold-start nor steady-state.
• No variance. The column the benchmark labeled "p95", shown above as Max, is the maximum of five samples, not a percentile. No confidence intervals exist, so the 7 percent difference between variants 2 and 4 is not established as meaningful.
• No energy measurement. The benchmark's energy column is mean seconds multiplied by an assumed 15 watts. It is arithmetic, not measurement, and is omitted here.
• No crossover claim. A recorded "reuse crossover" value of 1 is a constant in the benchmark code, not a computed result.
• Separate measurements are not combined. An earlier single-call timing of the two verifiers (103.55 ms against 25.79 ms, about 4.01×) is a different measurement from the five-way means.

10. What the Research Disproved

A research program that reports only its successes teaches very little. The negative results below are kept because the surviving design is defined by what they ruled out, and because a reader attempting the same directions would otherwise be likely to repeat them.

10.1 Early counterexamples

These are mathematical examples, not executed tests.

10.2 Three shortcuts tested in software

11. Practical Genesis: The Restricted Preview

11.1 What it is

The surviving implementation is a restricted, source-driven toolchain over a finite subset of two package grammars. It derives its verifier from canonical source and policy bytes, checks recorded executions against the derived expectation, tracks delegated authority in the four-state model, supports interrupted runs with recovery witnesses, and keeps locally authenticated custody of its history. Its command surface is seven commands: check, run, verify, recover, audit, keygen and rotate-keys. It is a toolchain for one user on one host. It is not a general-purpose language, not a distributed system, and not a deployed safety system.

Sections 11.4 to 11.7 show a real program in this language as run by the independent reviewer, what its recovery did and did not establish, a second program the reviewer wrote from the documentation, and a conventional comparison.

11.2 Independent acceptance

Throughout this paper, "independent reviewer" means a separate AI agent, recorded as Kimi K, that did not build Genesis and worked from a clean install in the Foundation's own environment. It is not an independent human research team or another institution, and its work is a check, not a replication.

The independent reviewer ran a clean-room adversarial review of the frozen eighth release candidate (RC8): a byte-identical offline rebuild of the distribution, matching hashes for every installed module, a nine-step product workflow, and retests of five counterexamples that had made the previous candidate not ready. The verdict was conditionally ready for restricted private preview: six gates passed, six were conditional, none failed. This is not an acceptance of a general Genesis language, and it does not cover the later projection and cache experiments of §7 to §9.

Gate 06 is the same 272-case check that §7 re-derives. It is a checked property of the frozen preview, using the preview's own verifier, and is distinct from the later 32-call optimization.

11.3 The correction history is part of the result

The previous candidate failed review on five reproduced defects in key custody and audit. Each became a regression test and was retested against the installed RC8 distribution. Two boundaries remain documented: data stores rotated under the earlier candidate fail closed rather than migrating, and one local race condition is accepted within the single-user threat model. The review's limits matter as much as its verdict: fourteen process-abort interruptions across seven key-rotation boundaries left the key-rotation state consistent (this concerns key custody, not recovery of workflow tasks), which is evidence about a process being killed and not about a machine losing power. Security-relevant implementation detail is kept here at the level of reviewed behavior.

The correction history did not end with the acceptance review. A later independent developer evaluation of the same frozen release found a defect that the acceptance review had not: the recover command can report success for a recovery that failed (§11.5). It is recorded here, alongside the earlier defects, for the same reason.

11.4 A program, independently executed

The program below is the preview's own recovery example, a six-module logistics workflow, run on 24 October 2026 by the independent reviewer from a clean install of the frozen RC8 distribution. The listing is the complete agent module, which holds the two required entry points: solve, the workflow, and resume_unknown, the recovery procedure. The other five modules (planner, compliance, coordinator, executor and status) are summarized after it, and the status module is shown in full because recovery depends on it.

Listing 1. agent.gsp6, complete module (2,390 bytes; SHA-256 5fdd3fa38a5d5f6a13b261443c390ab4e0cb770fe0af46e5acc21fce6bb1e5d8). Package identifier 2716ebc78d1eec0087402ff84d3951aa2bf5c558f13298cce107df79dce10ffa.

!gsp 0.6!module agent!version 1!import planner 1!import compliance 1!import coordinator 1!import executor 1!import status 2@role solve/entryfn solve(shipment_id, depth, policy, root_relation) -> SolveOutcome issues(P_manifest, P_hop_primary, P_hop_secondary, P_hop_escrow, P_park_hold, P_cut_sel) {@role solve/planner/call  let plan_word = call planner.plan_three_inv_dag(shipment_id, depth);@role solve/policy/cond  guard_policy policy on_false -> return ThreeInvPolicyDenied;@role solve/actorA/attempt  attempt effect_a consume(P_manifest) on_uncertain -> produce(ManifestUncertain) on_rejected -> return ManifestRejected;@role solve/compliance/forward_primary  call_forward compliance.vet_primary(shipment_id) forward(P_hop_primary) -> (SharedCommitUncertain, SharedCommitRejected);@role solve/compliance/forward_secondary  call_forward compliance.vet_secondary(shipment_id) forward(P_hop_secondary) -> (SharedCommitUncertain, SharedCommitRejected);@role solve/compliance/forward_escrow  call_forward compliance.vet_escrow(shipment_id) forward(P_hop_escrow) -> (SharedCommitUncertain, SharedCommitRejected);@role solve/actorA/park  park consume(P_park_hold) on_committed -> produce(ThreeInvParkCandidate) on_rejected -> noop;@role solve/actorB/select  bselect consume(P_cut_sel) root(root_relation) -> (selected, stale_rejected);@role solve/join  join_branches require_all_live forbid_untaken_candidates;}@role resume/entryfn resume_unknown(record, hist_proof, witness) -> ResumeOutcome {  crash_cut abandon_live clear_candidates;  restart_cut issue(R_read1, R_read2) clear_candidates;@role resume/load/match  load_decode record consume(R_read1) on_unknown -> reset_produce(ThreeInvLoadedUnknown) on_completed -> return ThreeInvCompletedVariant;@role resume/migrate/arm  migrate_v1 record requires(historical_proof) on_ok -> reset_produce(ThreeInvMigratedV2) on_missing -> return Rejected:no_hist_proof;@role resume/recheck/match  recheck_multi record consume(R_read2) fresh_from(R_read1) effects(effect_a, effect_shared_commit_inv1, effect_shared_commit_inv2, effect_shared_commit_inv3) -> (ThreeInvCurrentCand, WitnessManifestOnly, WitnessPartialCommits, WitnessAllThreeCommits);@role resume/forbidden  forbid unknown_to_completed, effect_replay, authority_mint, read1_reuse, unauthenticated_persist;}

Read as a workflow, solve issues six permits, consults a planner that is forbidden from side effects, checks a policy, attempts one outside effect (effect_a, the shipping manifest) by consuming one permit, and then delegates three permits across a chain of modules (compliance to coordinator to executor), where each is consumed only by the final call that actually attempts an effect. Every line beginning @role names the line that follows; those names become the step labels in the recorded trace and in verification. resume_unknown is the recovery procedure: at an interruption it abandons every permit still Live, issues two fresh read permits, decodes the stored record, migrates it if the record format has changed, and rechecks which outside effects the evidence actually covers. Its last line forbids, among other things, treating an unknown outcome as completed, replaying an effect, and minting authority.

Listing 2. status.gsp6, complete module. Status code 5 means Unknown under record format v1; recovery may migrate it to v2 only with historical proof.

!gsp 0.6!module status!version 2@role status/record/formfn parse_three_inv_record(raw_record) -> RecordValue {  forbid unbounded_int_cast, unknown_to_completed;}@role status/table/v1table v1 { 5 -> Unknown ; 8 -> Completed }@role status/table/v2table v2 { 8 -> Completed ; 9 -> Unknown }@role status/decode/rulefn decode_three_inv_version(raw_record) -> DecodedStatus {  forbid foreign_version_decode, completed_in_resume;}@role status/migrate/rulemigrate v1:5 -> v2:9 requires historical_proof yields ThreeInvMigratedV2

The remaining modules are short. planner declares a pure planning function. compliance has three vetting functions, each requiring its own permit and forwarding it onward. coordinator routes two of those on a named branch to either a shared-ledger commit or a rail shipment. executor holds the two functions that attempt outside effects. All six modules were checked and run as a single package.

Commands and captured output

The reviewer ran the commands below on Windows with the installed preview's own Python interpreter. A local signing key is created first and passed to run, verify and recover; key handling and the audit command are not shown. The run command deliberately interrupts the workflow after its first effect attempt. Output is reproduced from the reviewer's captured results; long digests are shortened and custody fields are omitted.

genesis-preview check   --pkg examples/recovery
genesis-preview run     --pkg examples/recovery --wal-db state.sqlite --key-file key.json \
                        --task-id T1 --crash-after-attempt 0 \
                        --emit-record interrupted.json --emit-cert interrupted.cert.json
genesis-preview verify  --pkg examples/recovery --record-file interrupted.json \
                        --cert interrupted.cert.json --key-file key.json
genesis-preview recover --pkg examples/recovery --wal-db state.sqlite --task-id T1 \
                        --key-file key.json --epoch-floor 1 --emit-record recovered.json

check    exit 0
  {"accepted": true, "package_id": "2716ebc7...0ffa"}
run      exit 0
  {"accepted": true, "result": "ManifestUncertain", "step_count": 4,
   "wal_custody": {"anchor_epoch": 1, "status": "INTERRUPTED_UNCERTAIN"}}
verify   exit 0
  {"accepted": true, "all_nine_accepted": true, "error_code": "ok"}
recover  exit 0
  {"accepted": true, "anchor_epoch": 2, "error_code": "ok", "verb": "recover"}

The first three results are what they appear to be. check accepted the source, including its authority typing. run stopped where asked: one permit consumed, five still Live, and the manifest effect recorded as unresolved rather than done. verify re-derived the expected behavior from the source and policy and accepted the recorded run on all nine of its judgments, bound to the exact source bytes. Those judgments establish that the record is a valid trace of this source under this policy; as §11.5 shows, a valid trace is not the same thing as a successful outcome. The fourth result is not what it appears to be, and §11.5 explains why.

11.5 Recovery: what the interpreter accepted, and what the command reported

Three different things can be meant when a run or a recovery is said to have "succeeded", and this paper keeps them apart throughout.

The investigation located the defect in the wrapper, and found that the interpreter and verifier behaved correctly when given correct inputs. The reviewer wrote an independent reference procedure that calls the same interpreter and verifier with the task's actual inputs: the real interruption point, the status code the program defines, the actual unresolved effect, and authenticated receipts. On the unmodified program it produced the nine-step trace below, which all nine verifier judgments accepted. Against deliberately bad inputs (an undefined status code, missing historical proof, an empty witness, and a witness claiming more effects than were unresolved) the same reference refused to commit and did not advance the epoch. The shipped wrapper, whose only test is that the trace is well-formed, would have committed three of those four.

What this does and does not establish. It establishes that the tested interpreter semantics are correct for this program and these controls: given the right inputs, the language reaches the right state and rejects the wrong ones. It does not establish end-to-end recovery correctness for RC8. Three facts keep the two apart. First, RC8 as shipped has no command that performs this recovery correctly; the correct result was reached only through the reviewer's own reference procedure, which has not itself been independently reviewed. Second, the verifier's nine judgments test whether a record is a valid trace of the program, not whether recovery succeeded: the failed recovery above was also accepted on all nine, which is why the verifier could not catch the wrapper's error. Third, the evidence covers one shipped program, one reviewer-written program and four negative controls. Whether recovery is correct end to end therefore depends on the wrapper being fixed and the whole path being re-tested (§15.2), and the paper treats it as unestablished until then.

Figure 9 sets the two recoveries side by side; Table 11.5 then gives the reference recovery step by step.

Table 11.5. Language-level recovery of the interrupted run (reference procedure, unmodified program). Counts are permits in each authority state after the step. One outside effect, effect:a, remains unresolved from step 3 to the end.

11.6 An independently written program, and a conventional comparison

To test whether someone other than the developer can program in Genesis from its documentation alone, the reviewer also wrote a new six-module program, a cold-chain customs and escrow clearance workflow, using only the preview's language, first-program, command and example guides. It exercises three vetting gates, two independent routing branches, and information-flow annotations that none of the shipped examples use. Its source is not reproduced here.

Adversarial probes. Twelve deliberate misuse attempts were all rejected with specific errors: malformed source and an unused permit; reuse of a permit already delegated; a direct leak of protected data to a public output; a one-line comment edit and an added annotation after certification; verification under the wrong key; a tampered ledger inside a recorded run; a duplicate task identifier; a retry that changed its inputs; recovery of an already completed task; repeated recovery of an already recovered task; and a key rotation onto a file the tool did not own.

Conventional comparison. The reviewer also wrote the same workflow as an ordinary Python program, which passed its five test assertions. The comparison is about where guarantees live, not about speed, and no timing comparison was made. Each guarantee below can be written in Python by hand; the difference is that RC8 enforced it, in the reviewer's tests, for every program its grammar accepts, from the source, without the programmer writing it again. These are observations about the accepted RC8 grammar under its single-user, single-host threat model; they are not claims about programs the grammar rejects, about other versions, or about attackers outside that model.

The last row matters as much as the others. The Python version can do things Genesis cannot. What RC8 currently offers is a narrower language in which a specific set of guarantees comes with the toolchain, within its accepted grammar and tested threat model.

11.7 What the language can and cannot express today

What a programmer can write. A package of modules, each with versioned imports; a required workflow entry point and a required recovery entry point; explicit permits that are issued, delegated across modules, consumed by effect attempts, and abandoned at interruption; named boolean branches; status tables with versioned record formats and migration rules; prohibitions the checker enforces (no side effects in a planner, no unknown-to-completed conversion in recovery); and information-flow annotations. Every line can carry a role name that appears in the trace and in verification.

What a programmer cannot write. The language is a finite workflow-specification language. It has no loops, no general arithmetic or expressions, and no direct network or file input and output; the reviewer's attempt to add a loop was rejected by the parser. Outside effects are simulated tokens rather than calls to real carriers, banks or escrow services. Both entry points are mandatory even for programs that do not need recovery.

Rough edges found by the reviewer. The information-flow annotations work but are not documented, and branch names that do not follow an internal naming pattern must be declared explicitly once any annotation is used. Running a program with a syntax error, instead of checking it first, prints an internal error trace rather than a structured message. Local recovery cannot undo physical outside effects, and it cannot detect a whole-file rollback of its own database unless a known epoch number is retained separately.

None of these limits is unexpected for a restricted preview, and none affects the verification results above. Together they mark the distance between the preview and a general-purpose language; closing that distance is listed in Figure 10 as a hypothesis, not a result.

12. Relation to Prior Work

Almost every ingredient in Genesis is established, and the paper does not present any of them as new.

• Exact summaries. The observation-relative summary is the quotient of a labeled transition system by a bisimulation or trace-equivalence relation, computed by partition refinement, and Theorem 1 is the completeness condition of abstract interpretation in its simplest form.
• Composition. Compositional exactness arguments follow assume-guarantee and rely-guarantee reasoning.
• State-space reduction. Partial-order reduction and abstraction refinement in model checking eliminate redundant exploration by proving that paths or states are interchangeable; the symmetry-sampling failure of §10.2 is the failure such methods are designed to avoid.
• Reuse of computed results. Memoization, partial evaluation and content-addressed incremental builds all eliminate repeated work; the projection of §7, which answers questions about every prefix of an execution from a single run, is closest in spirit to these.
• Recovery and external effects. Write-ahead logging and repeatable-history recovery, idempotency keys, outbox tables and event logs, and compensating transactions are standard practice. Systematic exploration of crash states has found real consistency bugs in storage software, which is also the clearest reminder that a finite set of tested interruptions is not a proof.
• Authority. Delegable, non-forgeable authority follows the capability tradition, and authority as a resource that cannot be duplicated or revived parallels linear types.
• Authenticated history. Hash-linked structures for tamper-evident records underlie the separation of compact state from verifiable evidence.
• Limits on distribution. Agreement among unreliable hosts carries known impossibility results, and exactly-once effects at a non-cooperating receiver cannot be guaranteed by the caller alone; both bound what Genesis can claim.
• Verified systems. Formally verified kernels and compilers show that strong guarantees are achievable for real software, and also that each guarantee covers only what its specification states.

What Genesis claims is narrower: a joint treatment, in one restricted toolchain with independent review and preserved counterexamples, of source-derived verification, delegated authority with a non-resurrection property, uncertain external effects, authenticated recovery, and observation-specific evidence. Whether that combination is new is a separate question, answered neither by this paper nor by any benchmark in it. A formal novelty and prior-art review has not been completed.

13. Broader Implications

The results suggest possible uses. They do not demonstrate them. Figure 10 places every capability discussed in this paper by the strength of its evidence; the table after it separates what the evidence shows in each application area from what remains a direction.

One implication is already supported. The research record itself contained four reporting conflicts (the number of authority maps, the Q5 count, the 546 and 272 figures, and several specification-versus-result mismatches) that were caught only because claims were labeled, sources were preserved, and numbers were recomputed from code. For a program carried out largely by AI agents, that is not incidental. It is evidence that the discipline Genesis applies to computation, stating what each summary preserves and re-checking it, is also the discipline AI-assisted research needs.

14. Known Limitations and Threats to Validity

These limits are part of the research record. They are not reasons to discard the supported results, and the supported results are not reasons to set the limits aside.

15. If This Paper Is Wrong, and What to Test Next

15.1 Falsification criteria

The central claims should be considered weakened or refuted if any of the following is found:

• A projected record differs from the record of an actual interrupted run, on any program that satisfies premises (a) to (d) of Proposition 2.
• Any sequence of operations accepted by the Genesis implementation moves a permit from Consumed or Abandoned to an active state.
• The 3.07-fold gain over the cache-only variant disappears under independent re-measurement with variance reported and without allocation tracing.
• The cost of computing and checking projections grows fast enough with program size, B or M that the net saving vanishes on realistic programs.
• A conventional implementation can state and check the same preconditions with comparable effort and comparable error rates, which would leave the Genesis architecture without a distinct contribution.

15.2 The research agenda

• Generalize the projection. Either prove Proposition 2 for a stated interpreter semantics, or test it with generated programs against the interpreter, including asymmetric branches and prefix-dependent external counts.
• Sweep the parameters. Vary B and M and confirm that interpreter calls follow 2·2^B(M + 1) + 2 for the baseline and 2·2^B for the projection.
• Measure properly. At least 30 runs per variant, cold and warm reported separately, memory measured in a separate run, variance reported, and an independently written conventional implementation alongside the algorithm-matched one. Measure energy or report none.
• Test the real hypothesis. Compare the rate of incorrect optimizations when the same technique is applied with and without explicit preconditions. This, not speed, is where Genesis would have to show an advantage.
• Test developer usability. Establish whether people other than the developer can write, check and recover Genesis programs within the preview's scope.
• Measure the missing levels. Implement Q3 and Q6 and report their sizes.
• Replicate independently. Have the developer experiments repeated by someone other than the developer, then update the claims ledger.
• Fix and re-review recovery. Correct the RC8 recovery command so that it resumes from the recorded interruption point with the program's own inputs and commits only a valid recovered result, then have it independently re-tested against the positive and negative cases of §11.5.

15.3 A separate technical paper

The work-elimination result deserves its own publication, because it is the program's strongest deterministic result, has a clear negative companion in the failed shortcuts, and needs more space for assumptions and method than a foundational paper can give it. The Foundation intends to publish it once the generalization, parameter sweep, measurement and replication steps above are complete, under the working title Exact Crash-Cut Work Elimination: Projecting Interruption Observations from Terminal Traces.

16. Conclusion

Genesis set out to ask whether computation could be organized around explicit relationships between execution, authority, verification, state and recovery, so that some work could be inferred instead of repeated. The answer so far is narrower than the question, and more useful for being honest.

The program has produced a small set of durable results: an observation frame that keeps unresolved external outcomes explicit; an observation-relative account of exact summaries, including cases in which no summary exists; an authority algebra of seven transformation maps in which, provably, spent authority cannot return; a restricted preview that an independent reviewer found conditionally ready for private, single-host use, with which that reviewer wrote and ran programs from the documentation alone; and a finite work-elimination result in which 272 interruption cases are checked from 32 interpreter runs instead of 546. It has also produced a larger set of well-characterized failures: the hope of a single unifying calculus, the invertible flip, symmetry sampling, the helical law, the early architectural claims, and a recovery command that reported a failed recovery as a success. The failures are as much a result as the successes, because they bound what may be asserted.

The most important single finding may be the least flattering one. A conventional implementation that used the same projection ran almost exactly as fast. Efficiency here came not from a new language running faster, but from recognizing, under stated conditions, that re-running was unnecessary. Whether a language that makes those conditions explicit helps people recognize them more reliably is the question Genesis now has to answer.

Useful computation should be performed when necessary, inferred when mathematically justified, and verified according to the precise obligations the program must preserve.

Roles and acknowledgments

Desmond Iwuagwu E. originated the Genesis research program and directs it for EM Foundation for AI Research: he set its foundational question, research direction and standard of evidence, directed the AI research agents, and decided what would be pursued and published. AI research agents carried out much of the formalization, implementation and testing: the agent recorded as Sol (Codex) built and self-tested the preview and the post-preview experiments, and the agent recorded as Kimi K performed the independent RC8 review and the later independent developer evaluation reported in §11.4 to §11.7, including the programs, adversarial probes, Python comparison and recovery investigation. Claude (Anthropic) selected, reconciled and interpreted the evidence for this paper, drafted it under the author's direction, and re-checked key results against the original code. Authorship and the roles described here are scientific attributions and are distinct from legal inventorship, which this paper does not address. The paper makes no claim that Genesis derives from earlier Foundation investigations; the located records contain no primary evidence either way.