Research
68 papers about the language, its checker, its runtime and the way agents use it. Each page says what exists on main today and what kind of result is still missing, so you can tell a measured claim from a design.
Every paper here is a draft. None has been peer reviewed.
The drafts were written against revl commit
45bec431f,
and the repository references in them link to that commit, so a reference keeps
meaning what it meant when it was written even as main moves. A citation
that still has to be checked is marked in the text.
Author: Thomas Moussajee. Text licensed CC BY 4.0. The sources are in the repository.
The checker, the rejection corpus and the guarantee table are on main with tests; the Lean models cover the rule lattice but not the Python checker, and no evaluation on third-party code exists yet.
Lean theorems for teardown, WAL discharge and no-residue and a differential oracle against the Python runtime are on main; roll-forward, failure during teardown and cascading abort are not modelled, and no mutation study of the oracle exists.
The three gate scripts, the registry and the differential oracle are on main with a current census; no gate-firing history, automated mutation study or registry audit exists yet.
The accumulation analysis is on main with deterministic element-copy counts on Python and TypeScript, and the owned/borrowed checks have tests; no timings, no soundness argument and no real-code coverage numbers exist, and shared handles are specified but not built.
The colour fixpoint, monomorphization, caller-decided extern colour and the self-colouring fix are on main with tests and a Lean fragment; colour polymorphism as a type-system feature is not built, and cross-tier evidence for go, java and rust is mostly emitted shape, not executed behaviour.
The v1 stream surface is on main with executed scenario tests on py and, where the toolchain is present, ts, go, java (against a stub API) and rust; durable replay is py only, and no external-workload evaluation or mechanization exists.
Cardinality analysis, budget ceilings and the SLO contract (compile-time gate, observed half, live producer, rollout gate) ship with tests on main; no precision, soundness-at-scale or overhead evaluation yet, and the check that links an SLO bound to the cardinality verdict is designed only.
Checker and Python runtime fan-out ship on main with tests; the TypeScript runtime fan-out and divert-aware cancellation do not exist, and there is no workload evaluation.
Mechanism and filesystem catalog ship on the Python tier with a dense test base; the TypeScript tier is partial (weaker guard, no directory-fd syscalls); no overhead or corpus-scale evaluation yet.
Seven audit findings are fixed on main with executed reproducers and regression tests on the Python and TypeScript tiers; the swapper measurement is a single run, the Node tier narrows but does not close the directory-swap window, and there is no external baseline comparison.
Shell classifier and lowering onto the witnessed filesystem catalog ship on the Python tier with tests, and the OpenAPI compensation routes ship; the touch-on-existing-file runtime split could not be found on main, and there is no real-traffic, differential or live-API measurement.
The teardown contract and the Python tier ship with tests; the six-tier conformance gate is only partly verified, and there are no measurements, saga baseline comparison or mutation study yet.
Commit protocol, deferral queue, abort and crash recovery are shipped on the Python tier with tests and a small measurement; witness retention is design-only and no external evaluation exists.
WAL, recovery, call-tier re-issue and model-versus-world labelling are shipped with crash tests on five tiers and a differential check against a Lean model; no overhead numbers or real-signal kill campaign yet.
Fault sweep, cross-tier sweep and round-trip tests are shipped with tests; no corpus-wide results, mutation analysis or baseline comparison yet.
Seeded scheduler, shrinker and auto-mocks are shipped on the Python reference tier with tests; no bug-finding or coverage measurements, and the deadlock check has no test.
Step-back, forward replay, bisect and the MCP verbs are shipped on the Python tier with 49 tests; no overhead or user-study data, and inverse correctness never reaches the bisect report.
Policy reader over a WAL and action reader over a session log are shipped with tests; no incident corpus, fidelity measurement or causal-cone computation yet.
Sealed model-decision evidence, an offline reader and a replay-readiness planner are shipped on the Python tier with tests; no replay mode is executable and no evaluation exists yet.
A serial, single-workspace fork with offline lineage tooling is shipped on the Python runtime with unit and integration tests; parallel copy-on-write branches, live branch re-execution and the language fork form are not built, and no evaluation exists yet.
The proposal and commit loop, undo as a gated change, the gauntlet dossier and a repair loop are shipped with tests; the edit verb existing clients call first still commits by default, two dossier slots are unwired, and no outcome evaluation exists yet.
The guarantee decode table, realms, the balancing pattern, the conformance matrix and the fork audit are on main; local realms are confirmed on four of five language tiers (the fifth depends on a change outside this tree), instance-parametric components exist on one tier, and no comparison against Cordis itself has been run.
The declared hand-off gate, warm start and undo reporting are shipped with tests on the Python tier; the default instance-migration path has a named, test-pinned, unfixed correlation hazard, and no measurements exist.
The halted verdict, the latch protocol on the Python tier and three native placement runners, the conductor and the Lean layer are shipped with tests; the Node tier does not yet honor the latch, wasm is reported statically, the cross-tier conformance fixture does not exist, and no latency or fault-injection measurements exist.
Fixes and per-bypass regression tests for seven generation-boundary bypasses are on main; no study design, detector or survey yet.
Row table, layered patches, fold, incremental admission and authority panel are built and tested on main (136 test functions); no evaluation, and runtime activation of a patched composition is not built.
Emitter, golden output, retry derivation and a live dev-server saga test exist on main; signals, timers, realms, versioning and the Python SDK target are not built, and no fault sweep exists.
Per-component tier placement and a py-to-py live swap with receiver-side re-admission are shipped and tested on main; no cross-tier swap test, no non-py seam admission, and no latency or gap measurements.
Attestation chain, coordinated prepare/commit/abort, boundary taxonomy and federation are shipped and tested on main; the SSH leg is tested through shims only and there is no fault-injection evaluation or replicated coordinator.
Container-rung sandboxing and the attestation verifier with delivery ledger are shipped and tested on main with synthetic quotes; wasm-cell and microVM rungs do not host components, and no overhead or real-hardware quote exists.
Seam row, remote row, A2A binding and adapter predicate are shipped with tests; seam runtime behaviour, transport-failure withdrawal and the observer value are not established, and there is no evaluation.
Admission, signed receipts, evidence recount, loopback dispatch with a one-result ledger and the tier ladder are shipped with tests; lawful retry is a kernel not wired into dispatch, and nothing runs over a real network.
The drift predicate, version derivation, contract check and registry publish gate are shipped with tests; there is no empirical study on real package histories and no formal soundness statement.
Admit-at-add, admit-at-assemble, search-as-admission, evidence-ranked resolve, adapter proposals, reproduce and the bootstrap fixpoint are on main with tests; the trust graph, adapter marketplace, hosted registry, signing and the reuse hint are not, and there is no evaluation.
The rule is proved in Lean over an abstract flow model, the checker is shipped, and component-body walk coverage is decided on a corpus; the interprocedural fixed point is unproved and there is no agent-benchmark evaluation.
The static rule, a Lean proof over an abstract model and the runtime registry on five backends (a refusal on the sixth) are shipped with tests; the trace funnel covers three tiers, the value channel none, and no evaluation exists.
The compile-time refusal and both signed receipts are shipped with tests; the deadline is per policy and not per value, derivatives are declared and not inferred, and no evaluation exists.
In-process spawn attenuation and the Lean ceiling theorems are shipped with tests and a differential oracle; the peer-placement edge and the lease and sandbox slices are design-only and no evaluation exists.
The audit surface, drift gate, policy leg and profile tool are shipped with tests, and the load-bearing Lean statement is the lattice form; no empirical evaluation on real regeneration traces exists.
The completeness harness, the jail path enumeration and the extern reach declaration are shipped with tests; the hole count and the claim that the harness would have caught the original holes are not backed by a replay.
The compile-time half and the approval-gate half are shipped with tests and a controlled 4-by-2 matrix; the lease path and a verb vocabulary at the gate are open, and no realistic case study exists.
The HMAC envelope pair and the reproducible bundle are shipped with tests; the drift monitor and asymmetric signatures are designed and not built, and no systematic evaluation exists.
The refuse-only gate, the drift gate, the import-free component and its conformance vector are on main with tests; the latency headline belongs to the Python gate, not to the Rust or wasm forms, nothing is published to a registry, and agreement and cost studies at scale are still needed.
Protocol, verbs, receipt, signed casts and HTTP transport are on main with tests; the count is of credentials, never of people, and there is no attack evaluation, overhead measurement or related-work survey yet.
A native source-to-source chain exists on main and is byte-exact on enumerated corpora (401 of 403 documents by the residual ledger); the self-host type checker is not the reference checker, there is no bootstrap fixed point, and the defect census and mutation analysis are still needed.
The coverage ledgers, ratchets, provenance sidecar and census are on main with tests and CI steps; the headline coverage figure is dated 2026-09-02 and needs a re-take, and the yield study (do closures find real bugs) has not been done.
The generated matrix, executor, drift gate and Lean theorem are on main; execution covers 19 of 61 constructs on three default tiers (rust and java behind a switch), the theorem is not yet bridged to the matrix, stream exit discipline is partial, and no divergence statistics exist.
The fuzzer, its tests and 13 regression fixtures are on main, but no campaign log, totals, baselines or CI run exist, so the findings rest on roadmap text and the type-directed claim has no ablation.
Decisions, docs and per-tier probes are on main for strings, integers, division, map order and mangling; the cost figures are single prose measurements and there is no divergence ledger yet.
Six per-backend audit harnesses and their before/after counts are on main with tests pinning most fixes; there is no uniform cross-backend corpus, no timing validation and one correctness defect found is still open.
Five importers and an export direction are on main with about 250 tests and two executed generator-injection fixes; no corpus-scale evaluation and no measured error rate for the weakening rules.
Derivation traces, runtime causes with a withdrawal oracle, and navigable refusals are on main with named tests and CLI/MCP surfaces; no agent-side or human-side measurement yet.
Mechanism, tests and a formal model row are on main; there is no measurement of prompt burden or of false auto-approvals yet.
Admission, the untrusted-author profile, the in-process admit crossing and the MCP trust default are on main with tests; the only measurement is 5 scored attempts on one model, and physical confinement of host code is designed only.
Hint derivation and the gating proxy ship on main with 26 proxy tests and 8 adversarial hint tests; no corpus evaluation, no overhead measurement and no mechanized proof of the hint projection yet.
Operator profiles, per-verb gating and completeness tests ship on main with about 38 unit tests; no bypass study, baseline comparison or agent evaluation yet.
Controller, kernel capability, layer-state registry and promotion barrier ship on main as a first slice with synthetic differential corpora; stage adapters, a computed authority diff and lifecycle wiring of rollback are designed, not written.
Python tier ships Gate.propose with a health-gated swap and named tests; the Rust host cannot swap, re-entrant propose is refused, and no live-model evaluation or performance measurement exists.
Python tier and the promotion decision procedure ship on main with constructed-evidence tests and mutant runs; five tiers are unwired and no live shadow run has been done.
Derivation, seam, two dialects and the retry budget ship on the Python tier with structural tests and a small provider probe; retry reduction is not measured and the call-site generic form is not built.
Declaration, placement ceiling, answer type, per-member inputs, a self-host port and a partial formal row are on main with test suites; no runtime aggregator exists and nothing has been evaluated on users or benchmarks.
Static classification, rungs, target binding, receipt, a failure-keyed compensation run and tier runtimes are on main with tests; there is no real GUI substrate, no end-to-end evaluation and no unconditional confirmation gate.
The four roles and the check/admit surface are shipped with tests and a measured admission latency; the lighthouse admission loop is a roadmap proposal and no agent-outcome study exists.
Scorer, sealed draw and mutation evidence are on main with tests; no model-produced trajectory has ever been scored.
Protocol, report checker, committed corpora and model-free rescoring are on main; the three-host comparison covers 3 of 30 briefs and the pinned-model run is incomplete.
The probe and an unload-surface survey are on main with fixtures and a self-check; a first measurement exists only on a self-authored 10-plugin corpus, and the population study has not been run.
Guard, switch and CI wiring shipped on main with tests; one-laptop before/after measurement exists, no history series or external replication yet.
Five gates and their tests shipped on main, four wired into CI; no catch-rate study, outside baseline or decay-share denominator yet.
Some drafts cover one argument from several sides. These groups are planned to become a single paper each; until then they are published as separate drafts.
Cite the collection, or a single draft from the cite block at the end of its page. A draft is a work in progress: cite the page, not a result as settled.
@misc{revlresearch,
author = {Thomas Moussajee},
title = {Research drafts about revl},
year = {2026},
howpublished = {\url{https://inso1337.github.io/revl/research/}},
note = {Collection of research drafts, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}