Model and node
Rholo
A Rust node for the ρ-calculus: native object capabilities, horizontal scale-out by design, and laws proved at the model and tied to the node.
- What
- Rholo is a Rust implementation of the former RChain node: Rholang and RSpace, Casper consensus, storage, networking, and OCapN, ported crate by crate from the preserved Scala reference.
- Why
- The common pattern puts concurrency in the runtime and authority in a permission check. RChain made both structural: processes compose with
|, and an unforgeablenewname is the authority. The port keeps that concurrent, replicated state machine running and tests its laws against a machine; the organisation dissolved in 2022. - The combination
- A ρ-calculus language where authority is a name and concurrency is native; a Rust node designed to shard horizontally; and a law register that ties machine-checked models to the running node by conformance corpora.
The model
| Model | Complete | Compositional | Concurrent | Mobile | Reflective | Behavioural types | Capabilities (of 6) |
|---|---|---|---|---|---|---|---|
| Turing machines | Yes | No | No | No | No | No | 1/6 |
| λ-calculus | Yes | Yes | No | No | No | No | 2/6 |
| CCS | Yes | Yes | Yes | No | No | No | 3/6 |
| Petri nets (plain P/T) | No | No | Yes | No | No | No | 1/6 |
| π-calculus | Yes | Yes | Yes | Yes | No | Yes | 5/6 |
| ρ-calculus | Yes | Yes | Yes | Yes | Yes | Yes | 6/6 |
Adapted from the Rholo README table; Mobility replaces Complexity; the score is an equal-weight capability count, not a ranking. Petri is plain P/T (extensions make Complete true); π/ρ behavioural-type marks denote existing systems, not maturity.
λ is substitution; π adds concurrency and mobility; ρ makes a name a quoted process (@P/*x); RChain embedded ρ as a base sort of a Calculus of Constructions (type system).
| Claim | Mechanism | What is established | Boundary |
|---|---|---|---|
| Horizontal scale-out | Shard routing; cross-shard invoke; two-phase commit (Laws 26–29); merge (Laws 9, 17); concurrent replay of dependency-free blocks. | The mechanisms exist in code and are modelled in Lean; this is not an end-to-end distributed run. | Single-shard default; transaction API off; no production benchmark. 60–160 deploys/s is derived, not measured. Residency Θ(N²): 16 GB ≈ 12 h at 2 s blocks. |
| Native object capabilities | Unforgeable new names; bundle facets; forwarders; revocation; sealer/unsealer; reflection; OCapN. | Possession is authority; capture-avoiding substitution is proved over the model (Law 3); the patterns are language constructs. | Move/Sui also make references unforgeable. The difference is proved capture-resistance, the o-cap patterns, and reflection; delegation safety remains a discipline. |
| Correct by construction | No unsafe in the 14 first-party crates; ρ as the base sort of a CoC; 100 of 109 entries non-vacuous; 23 entries tied to the node by conformance corpora. | Memory-unsafety is unwritable in first-party code; proved laws are machine-checked and, where marked, run against the node. | Not a whole-node proof. Dependencies, leaks, logic errors, denial of service, and consensus bugs remain. 2 entries vacuous; 7 not counted as proved (1 axiom, 1 open, 3 retired, 2 orphaned). |
Design
- A name is a quoted process. Reflection is primitive:
@Pnames a process and*xrecovers it. Bundles are read/write facets, forwarders attenuate, and revocation is a language pattern. Authority is a name, not a permission table. - The law register is the oracle. Corpora emitted from the register run 1:1 through the node. The Scala reference contributes vectors, not truth.
- Provenance is fixed before the port. Upstream is pinned and restorable, and its 165-file differential corpus is the reference’s surviving authority — as data, not specification.
- Assurance is written and gated. Findings have one home and close by construction; HAZOP, bow-tie, a bounded-adversary tabletop, fuzzing, and a coverage floor leave a re-runnable record; it is not independent review.
Provenance and rescue
Original: the Rust node, the Lean laws, the conformance corpora, and the assurance record. Inherited: the former RChain protocol and the upstream Scala, pinned at 1b7583649 and restorable with git checkout 1b7583649 -- legacy. A code snapshot at 14b8b77 is timestamped on Arweave, 22 August 2026. Rust is AGPL-3.0; upstream Scala is Apache-2.0. The port is a rescue in the plain sense: the code was preserved and the protocol continued. No ownership is claimed.
Public record: summarises public reporting; contested claims are attributed. Context for the engineering work, not an allegation.
| Year | Record | Source |
|---|---|---|
| 2017 | The cooperative forms to steward the platform. | GeekWire (2019) |
| Dec 2018 | After raising roughly $30–31M, it spends $23.5M on a five-year audio-codec license; The Block reports that sources described the treasury as “functionally bankrupt”; senior departures follow. Press characterizations, not adjudicated findings. | The Block (2018) |
| Feb 2020 | Mainnet launches with cooperative validators. | RChain announcement (2020) |
| Aug 2022 | The cooperative announces it is dissolved, citing legal, financial, and logistical issues; the network is left without a steward. | RChain Cooperative (Wayback, 2022) |
No individuals are named in this record.
Earlier continuity work: in 2024 I co-authored the RGov/Rhobot recovery proposal for REV/RChain with Jim Whitescarver; the old RNode was forked into the Gorki/BigSur project. The Gorki organisation, the old node fork, and the RGov repository are public.
The port is also a return to the RChain work I left unfinished in 2019–2022; that is part of why it exists.
I did not design RChain; this record covers the port and verification. Arweave snapshot · Legacy Scala tree · QuCalc research docs.
Evidence
| Measure | Value | Source |
|---|---|---|
| Rholang laws | 85 laws (109 entries) | spec/LAWS.md |
| Non-vacuous proofs | 100 of 109 entries | spec/LAWS.md |
| Laws tied to the node | 23 entries | spec/INVENTORY.md |
| Laws proved over the model | 77 entries | spec/INVENTORY.md |
| Vacuous proofs | 2 entries | spec/LAWS.md |
| Entries not counted as proved | 7: 1 axiom, 1 open, 3 retired, 2 orphaned | spec/INVENTORY.md |
| First-party crates | 14; 0 unsafe | README |
| Tests | 2,281 test functions (README, 15 Oct 2026) | README |
| Test ledger | 1,481 unit + 130 integration | Test coverage |
| Coverage floor | 87% (89.97% measured) | Coverage ledger |
| Self-adversarial review (T1 scope) | No P0; 3 P1, 4 P2, 14 P3 closed; 204/204 filed findings | Security audit |
| Upstream corpus | 165 files, run 1:1 (README) | README |
Sources: repository README and specification documents, as of October 2026. Counts drift; the linked artifact is authoritative.
Language and runtime
- rholang
- rspace
- qucalc
- graphz
Consensus and storage
- casper
- block-storage
- models
- shared
Networking and crypto
- comm
- ocapn
- crypto
Tools
- sdk
- node
- rspace-bench
Limits
- No external audit firm. The security record is a written, gated self-adversarial programme: the September 2026 pass found no P0 (chain split, fund loss, or remote code execution); three P1s, four P2s, and fourteen P3s were confirmed and closed. The review ledger still carries 507 deferred rows of 626, and the September pass read the T1 roster, not the whole tree.
- Formal assurance is layered. The register covers 85 laws across 109 entries. 100 entries are non-vacuously proved — 23 proved and tied to the running node by conformance corpora, 77 over the model. Two further entries are vacuous proof statements; seven are not counted as proved (one axiomatized by design, one open, three retired, two orphaned). The Coq track defines the α-equivalence metatheory but states its laws as axioms.
- Memory safety is first-party only. No
unsafecovers the fourteen crates, not their dependencies; it rules out the memory-unsafety class, not leaks, logic errors, denial of service, or consensus bugs. - Sizing is an estimate. The node is storage- and uptime-bound, not CPU-bound; RAM and start-up time scale with chain length. The hardware page carries measured start-up figures, not a production benchmark.
- Throughput is bounded and residency is superlinear. A block carries at most 255 deploys; the scaling page derives roughly 60–160 deploys/s on one shard and 6–20 s finality. Residency is Θ(N²): at a two-second block interval, 16 GB of memory is roughly twelve hours away, and sharding is untested at scale.