{"id":"670d862b-d862-4b9a-82f5-e956631de893","slug":"revl","kind":"mcp","name":"revl","summary":"A language for safe, universal spatiotemporal composability (Cordis paradigm) and orchestration.","owner":"inso1337","repoUrl":"https://github.com/inso1337/revl","license":"AGPL-3.0","licenseTier":"strong-copyleft","trust":"community","stars":8,"match":null,"fewStars":false,"format":"mcp","createdAt":"2026-08-16T22:03:41.000Z","addedAt":"2026-10-21T06:35:57.679Z","logoUrl":"https://avatars.githubusercontent.com/u/6376377?u=37a4ab9364e16bd8503af1faae73b40f9d9c4e3f&v=4","linkOnly":false,"collection":null,"skillPath":null,"categories":["developer-tools","memory-knowledge"],"tags":["cordis","ai-agents","ai-safety","capability-based-security","compiler","effect-system","formal-verification","programming-language"],"runtime":"python","local":true,"cloudCapable":false,"cloudCapability":"unknown","cloudReadyOnPlatform":false,"needsApiKey":false,"reviewed":false,"syncedAt":"2026-10-21T06:36:13.963Z","sample":false,"url":"https://conduits.dev/tools/revl","language":"Python","transports":["stdio"],"install":{"pypi":"revl"},"requirements":{"env":[],"upstreamMayCharge":false},"tools":null,"readme":"
\n\n\"revl:\n\n

\n \"CI\"\n \"6\n \"validated\n \"self-hosting\"\n \"MCP\n \"AGPL-3.0-only\n \"DOI\"\n

\n\n

\n Quickstart ·\n What makes it different ·\n Documentation ·\n Design ·\n Vision ·\n For agents\n

\n\n
\n\n---\n\nrevl is a language for software that changes while it runs. Components\nload, unload, and hot-swap inside a live system, and the properties that make\nthat survivable are checked at compile time: unloading leaves no residue,\ndependencies stay coherent, nothing reaches state it never declared. The core\nmove is small and strict. Every mutation is written beside its inverse, and a\nmutation with no inverse, one that crosses the system boundary, must carry an\n`emit` marker at the call site. Irreversibility is legal; invisible\nirreversibility is not.\n\nThe paradigm comes from [Cordis](https://github.com/cordiverse/cordis) and the\npaper it implements, [*A Programming Paradigm for Spatiotemporal Composability*](https://github.com/cordiverse/paper).\nThe paper proves strong theorems about revertible effects, but each one rests\non hypotheses a library can only ask programmers to respect. revl moves those\nhypotheses into the checker. C++ had RAII as a discipline and Rust made it a\ntype system; Cordis has revertible effects as a discipline and revl makes them\na language. The borrow checker governs lexical resource scope. revl's checker\ngoverns dynamic component scope: what may enter a running system, what it may\ntouch while there, and what must be true when it leaves. What this project\nclaims, and what it deliberately does not, is [docs/vision.md](docs/vision.md).\n\n```revl\nservice Database {\n emission fn execute(sql: Str) -> Int // crosses the system boundary\n}\n\nservice Cache {\n fn get(key: Str) -> Opt[Str]\n emission fn put(key: Str, value: Str) // its body emits, so the interface says so\n}\n\ncomponent UserCache requires db: Database provides cache: Cache {\n let store = effect Map.new() undo store.drop() // every effect declares its inverse\n\n provide cache {\n fn get(key) = store.get(key)\n fn put(key, value) {\n effect store.insert(key, value)\n undo store.remove(key)\n emit db.execute(`INSERT INTO cache_log VALUES (${key})`)\n }\n }\n}\n```\n\nRead that as a contract the compiler enforces. Drop the `undo` and it will not\ncompile. Call `db.execute` without the `emit` marker and it will not compile.\nReach for a service the component never required and it will not compile.\nDeclare `put` as a plain `fn` while its body emits and it will not compile: a\nservice declaration is an upper bound on what its providers may do. Teardown is\nderived, LIFO over exactly the effects that ran, and an `undo` body has no way\nto register new effects because the grammar gives it nowhere to put one. Link\ntime rejects dependency cycles and two providers of one key. Nine guarantees,\nG1 through G9, are the table in [DESIGN.md](DESIGN.md). G1 through G8 each\ndischarge a hypothesis the paper could only ask programmers to respect. G9 has\nno paper anchor: it is revl's own, and it is where this project stops packaging\nthe paradigm and starts extending it.\n\n## Quickstart\n\nrevl needs Python 3.11 or newer and is installed from source. The name `revl`\non PyPI belongs to an unrelated project, so do not `pip install revl`.\n\n```bash\ngit clone https://github.com/inso1337/revl && cd revl\npython3 -m venv .venv && source .venv/bin/activate\npip install -e .\n```\n\nWith [uv](https://docs.astral.sh/uv/) the last two lines are\n`uv venv && source .venv/bin/activate && uv pip install -e .`. To install a\ntagged release without a checkout, use\n`pip install \"git+https://github.com/inso1337/revl@\"`, with a tag from the\n[releases page](https://github.com/inso1337/revl/releases). To run the test\nsuite, install the extra (`pip install -e \".[test]\"`) and run `pytest tests/`.\n\nWith the virtual environment active, `revl` is on your PATH:\n\n```bash\nrevl compile examples/user_cache.rvl # source -> checked IR, printed as JSON\nrevl emit examples/user_cache.rvl # source -> emitted TypeScript (--backend picks another tier)\nrevl audit examples/user_cache.rvl # everything that can cross the boundary\nrevl mcp serve # the compiler as an agent admission gate\nmake demo # a live hot-swap, migration and rollback\nmake demo-flagship # one agent, ten steps, six refusals\n```\n\n`make demo` needs more than the install above: it runs\n`backends/python/setup.sh` on first use (git, uv and network access) to build\nthe runtime it hot-swaps on. `revl mcp serve` prints the same pointer if that\nruntime is missing and starts with the live verbs unavailable.\n\nThe `revl` console script is the documented happy path. The\nabsolute-interpreter fallback is `python -P -m revl` (PYTHONSAFEPATH, 3.11+).\nThe `-P` matters: without it, the current directory can shadow the installed\npackage (issue #336; issue #317 is the underlying mechanism).\n\nThe language reference is [docs/syntax-2.0.md](docs/syntax-2.0.md); if the\ncomponent author is a model, start with the\n[agent guide](docs/guide-ai-agents.md) instead.\n\n## What makes it different\n\n### The undo is checked, not hoped for\n\nUndo logic is the classic write-only code path: written once, wrong quietly,\nexercised at the worst possible moment. revl refuses the quiet part. Code\noutside `effect` forms is pure, so the accumulator provably holds every\nmutation, and the emission marker keeps the two kinds of change, revertible and\nnot, distinct in the types. When a component deactivates, the runtime replays\ninverses in reverse order and the environment is exactly what it was before\nactivation. That property is what the whole language is shaped around.\n\n### The gate defends against the component's author\n\nThe reversibility theorems come from the paper. The admission gate does not.\nrevl treats its input as hostile, because increasingly that input is written by\nan agent optimising for \"make the tool say yes,\" and such an author will phrase\na side effect however it must to slip past a name-based check. So the checks are\nnot name walks. When a generated MCP tool advertises `readOnlyHint: true`, revl\nhas proved the operation reaches no irreversible host effect, through an emission\nfixed point that follows an effect even when it is handed around as a value and\nfired one indirection later. An effect that escapes its declaration does not\ncompile.\n\nOn top of the eight paradigm guarantees, revl adds a security discipline the\npaper never described, enforced by the same checker. G9 refuses authority\nmanufactured from untrusted data unless a declassification is declared and\naudited, a static defense against prompt injection. Capability-bound `Secret`\nvalues cannot reach a log, a serializer, an LLM prompt, or an undeclared\nreceiver. A further family of rules governs async boundaries, acquisition order,\nand provider signatures. The properties an attacker would have to break, and the\nexecutable suite that tries to break them, are in\n[docs/threat-model.md](docs/threat-model.md).\n\n### One front end, six live runtimes\n\n
\n\n\"one\n\n
\n\nOne front end parses, checks, and links `.rvl` into a single IR. Six emitters\nlower that IR to six hardened Cordis runtimes: cordis-py (reference), cordis\n(TypeScript), cordis-rs (Rust), cordis4j (Java), cordis-go (Go), and the\nfirst-party cordis-wasm sandbox. This is not six ports of a demo. Components\nbuilt for different runtimes compose in one running system across process\nboundaries, a Python component consuming a service a Rust component provides\n([docs/interop-bridge.md](docs/interop-bridge.md)). And the claim that all six\ntiers agree is measured, not asserted: every construct is emitted through every\nbackend and the output is handed to that tier's real compiler, `tsc`, `cargo\ncheck`, `javac`, `wasmtime`. The construct-by-tier matrix lives in\n[docs/conformance.md](docs/conformance.md), regenerated by `make matrix` and\ngated in CI. Where a tier genuinely cannot agree, the conformance suite pins the\ndivergence and names it rather than hiding it, so a difference between runtimes\nis a documented fact instead of a surprise in production.\n\n### The compiler is the agent's interface\n\nIf components are increasingly written by AI agents, the question that matters\nis whether a generated component is safe to deploy into a system that is\nalready running. revl's answer is to make the compiler the admission gate.\n`revl mcp serve` (to connect it to an MCP client working on your own project,\nsee [the client recipe](docs/guide-ai-agents.md#wiring-revl-mcp-serve-into-a-working-session))\ngives an agent `revl_check` and `revl_admit` instead of\nfilesystem access: drafts are held server-side, edited by delta, and nothing\nlands until the same checker that guards human commits says yes. A rejected\ncandidate cannot deploy, and every rejection carries the guarantee it violated\nplus the rewrite that fixes it. Tool safety annotations are derived from the\nmethod body rather than asserted by an author, so a tool cannot call itself\nread-only when it emits. One tracked run of the Python gate measured the\nin-process `compile_source(..., manifest=running)` round-trip at a median of\n**0.165 ms** for a small candidate against a two-component running composition\non an Apple M1 Max / Python 3.14.3. This is not MCP transport latency.\n`tests/test_admission_latency.py` holds a 20 ms ceiling, which is only a\nregression guard, not a performance claim. See the\n[measurement](bench/results/admission-latency.md) and a\n[worked MCP admission example](docs/mcp-admission-walkthrough.md).\n[docs/mcp-bridge.md](docs/mcp-bridge.md) has the shapes;\n[docs/guide-ai-agents.md](docs/guide-ai-agents.md) has the workflow.\n\n### Tooling that operates a running system\n\nBecause the compiler knows every effect and its inverse, it can answer\nquestions no ordinary toolchain can. The `swap` verb of `revl run --placement`\n(a REPL verb, not a `revl` subcommand) migrates a live component to another\nruntime tier, re-pointing every consumer across the cutover and ending with a\nproof the old provider left nothing behind\n([docs/swap.md](docs/swap.md)). `revl plan` shows the exact delta a hot-swap\nwould produce and `revl apply` executes it with a derived rollback, so a\nmid-plan failure unwinds by inverses instead of by hand\n([docs/plan.md](docs/plan.md), [docs/apply.md](docs/apply.md)). `revl why`\nprints the derivation behind a rejection or a runtime transition\n([docs/why-traces.md](docs/why-traces.md)).\n\n### Placement is an isolation boundary, not just a tier choice\n\nA component can declare an isolation boundary and a capability envelope, no\ndisk, no network, or an explicit allowlist, and run inside a wasm cell, a\ncontainer, or a microVM while still composed with the rest of the system over\nthe ordinary process seam (value copy, audited crossings). The envelope is\nchecked statically and enforced at runtime: a component whose declared\ncapabilities exceed the sandbox grant is refused before anything launches, and\ninside the boundary the container runtime or hypervisor is the enforcer. That is\nwhat turns the untrusted-author and taint guarantees from checked into\nphysically enforced, since an opaque host body confined to no network cannot\nexfiltrate what the audit cannot see inside it. The ladder runs from wasm cell\n(in process, weakest) through container to microVM (its own kernel, strongest),\none capability contract at three enforcement strengths. The container rung hosts\na component today, and the microVM rung boots a guest and confirms the boundary\nfrom inside, with in-guest hosting the next step\n([docs/design/411-sandbox-placement.md](docs/design/411-sandbox-placement.md)).\n\n### Deployment is a coordinated transaction, not a copy\n\n`revl deploy` admits a deployment map and drives a coordinated PREPARE then\nCOMMIT across the composition's participants, so a partial failure rolls back in\nreverse commit order instead of leaving a half-applied system. When the\ndeployment names an attested bundle, the receiver re-verifies the whole chain,\nfrom source to IR hash to artifact hash to capability policy to evidence to\nsignature, by re-hashing the bytes it will actually run rather than trusting the\nattestation's own claims, and refuses to load anything whose hash, backend,\ncapabilities, or policy drifted. Every effect that crosses a boundary carries a\ncorrelation identity for recovery and duplicate detection. The coordinated\nmulti-process deploy runs today; the cross-machine leg, an ssh runner that\nspeaks the same protocol behind a pinned host key, is landing, and a replicated\nwrite-ahead log for partition-safe distributed commit stays deferred\n([docs/deploy.md](docs/deploy.md)).\n\n### Crash recovery is derived, not bolted on\n\nThe effect accumulator is already an ordered list of actions paired with their\ninverses, so it persists directly as a write-ahead log, with no separate recovery\nframework to write or trust. `revl recover` walks that log after a `kill -9` and\nreports, per effect, what is moot, what compensates, and what must be undone\n([docs/crash-recovery.md](docs/crash-recovery.md)). The engineering around it is\nwhere the guarantee actually has to hold. A reclaim fence closes the crash window\nso a half-written entry cannot be replayed as complete. Run-complete scoping\nstops a reused log from reporting a false CLEAN. An operator E-Stop strands the\nin-flight decision without tearing down what is still legitimately owned, and a\nre-armed disposer keeps that ownership rather than dropping it. This is the part\nthat matters for agents and distributed teardown, and it is where much of the\nrecent work lives.\n\n### What is proved, and what is deliberately not\n\nThe paradigm's metatheorems transfer by construction: the research claim is a\nsurface language whose every well-typed program satisfies the calculus's\nhypotheses, not new type theory. What revl proves in Lean is part of its own\nadmission judgment. In [formal/](formal/), G2 through G9 are `full` at the\ngranularity each row of the ledger states (the G4 and G8 shape-level statements\nare marked weak, and G6 is head-granularity): axiom-gated with no `sorry`,\ncarrying non-vacuity witnesses and, where the ledger records one, a differential\noracle against the shipped checker. G1 is `partial`, and the remaining rows are\npartial or still in progress, each for a named modelling reason, and\n`formal/STATUS.md` is the per-theorem ledger, written to be read gap-first. The live source of truth for the checker is still the\nimplementation and its golden and adversarial tests; the Lean layer is a growing\nbackbone under that, not a finished metatheory, and CI's `formal` job keeps the\ndistinction honest.\n\n### It compiles itself, and disagreement is a bug report\n\n`selfhost/compile.rvl` is the revl compiler written in revl. Where its native\npipeline runs today (59 of the 61 constructs in the conformance matrix, with no\nreference compiler in the chain), its output is byte-identical to the\nreference compiler, which makes self-hosting more than a stunt: two independent\nimplementations of one grammar run the same input, and any divergence is a real\ndefect in one of them. The two remaining constructs are `component/block effect setup` and\n`fn/verified fn`.\n\nThe self-host gate is not yet the reference gate. It does not implement the G5,\nG7, G9, A2, A8, A9, G-RETAIN and G-SECRET-FLOW checks, and it diverges from the\nreference on a few reproducers of G1, G2, G3 and G6.\n[docs/conformance.md](docs/conformance.md) has the per-construct `revl` column\nand the per-guarantee list of what the self-host gate does not refuse. The\ndefects this differential oracle has already caught are written up in\n[docs/selfhost-findings.md](docs/selfhost-findings.md).\n\nThe supporting cast is what you would expect from a checked language, done\nplainly: bidirectional type checking, no `null` (absence is `Opt[T]` and never\nsilently unwraps), exhaustive `match`, and an extern boundary that must\nclassify itself as `pure`, `acquire`, or `emission` before it compiles, so\n`revl audit` can enumerate everything a component could ever do to the world.\n\n## Documentation\n\nThe full index is **[docs/README.md](docs/README.md)**. Start here:\n\n- **[DESIGN.md](DESIGN.md)** for the guarantees and the checked table, **[docs/vision.md](docs/vision.md)** for what this is for and the honest scope of the claims\n- **[docs/guarantees.md](docs/guarantees.md)** the guarantees and rules at a glance, with origins (decode a cited `G4`, `T2`, or `A8`)\n- **[docs/syntax-2.0.md](docs/syntax-2.0.md)** the language reference, **[docs/stdlib-2.0.md](docs/stdlib-2.0.md)** the stdlib surface\n- **[docs/guide-ai-agents.md](docs/guide-ai-agents.md)** the agent workflow, **[docs/mcp-reference.md](docs/mcp-reference.md)** every MCP verb, **[docs/commands-reference.md](docs/commands-reference.md)** every subcommand\n- **[docs/conformance.md](docs/conformance.md)** every construct against every tier, **[docs/crash-recovery.md](docs/crash-recovery.md)** the WAL and what honestly survives a crash\n- **[CHANGELOG.md](CHANGELOG.md)** what changed in each release, **[docs/v2.0-roadmap.md](docs/v2.0-roadmap.md)** what is done and what is in flight, **[CONTRIBUTING.md](CONTRIBUTING.md)** the workflow and the pre-commit contract\n\n## Acknowledgments\n\nrevl is the language-level realization of\n[Cordis](https://github.com/cordiverse/cordis) and the paradigm of its\n[paper](https://github.com/cordiverse/paper); it exists because the runtimes it\nlowers to do. With gratitude to\n[cordis-py](https://github.com/geohotstan/cordis-py),\n[Cordis](https://github.com/cordiverse/cordis) (TypeScript),\n[cordis-rs](https://github.com/dshbox/cordis-rs),\n[cordis4j](https://github.com/1na-ko/cordis4j),\n[cordis-wasm](https://github.com/inso1337/cordis-wasm), and\n[stc-go](https://github.com/0xdenny218/stc-go), and to the toolchains that\nbuild and validate every tier ([pytest](https://github.com/pytest-dev/pytest),\n[TypeScript](https://github.com/microsoft/TypeScript),\n[Wasmtime](https://github.com/bytecodealliance/wasmtime),\n[Serde](https://github.com/serde-rs/serde), and more).\n\n## License\n\nThe compiler, the admission gate and the tooling are\n[AGPL-3.0-only](LICENSE). Everything that ends up inside your program, the\n`stdlib/`, the runtime shims under `backends/`, the examples, is\n[MIT](LICENSES/MIT.txt), and the code revl emits from your source is yours.\nThe split, file by file, is in [LICENSING.md](LICENSING.md). The names revl and\ntruc and the logo are trademarks; see [TRADEMARK.md](TRADEMARK.md).\n"}