R-Sure

An insurance market needs capital, a way to place a risk, a contract, and a claims process. R-Sure models the Lloyd’s version of that market in five parts.

A syndicate contributes capital and reserves capacity. A broker registers and opens a slip. Syndicates quote and subscribe. The customer accepts and funds the premium. The policy binds. A claim is notified, classified, assessed, agreed, and settled. The central fund covers a shortfall under governed, capped rules. Those five parts are the market; the rest of the page explains why it is built this way and what the contracts guarantee.

Lloyd’s is a marketplace, not an insurance company. Syndicates supply capital; brokers represent customers; a slip is the placing document; the lead syndicate sets the terms and followers subscribe; a policy binds it; claims are assessed and paid by each syndicate’s share.

That structure spreads a large risk across many backers and lets specialist capital take only the risks it understands. Its cost is coordination: the same risk, shares, premium, and claim record must be reconciled across firms. A shared ledger can remove some of that reconciliation.

The design comes from Dan Robles’ 2016 NAIC/CIPR paper, which argues that the point of a blockchain is to reduce the cost of capital by decentralising risk, and that insurance is where that happens. The paper also ties insurance to engineering: the engineering stamp is evidence of a project’s value, and insurability depends on engineering sign-off. R-Sure takes that as its brief. A risk submission records the three insurability questions — what is exposed, how likely is the loss, and what would it cost — and a claim can carry R-Gen claim, validation, K-Asset, and provenance references. A disputed claim can open an R-Gen oracle case for a credentialed adjudicator.

Seventeen contracts cover the market. A syndicate contributes capital and reserves capacity; a broker registers and opens a slip; syndicates quote and subscribe; the customer accepts and funds the premium; the policy binds; a claim is notified, classified, assessed, agreed, and settled. Each line pays once.

Subscriptions sum to 10,000 basis points, and the first line is the lead. The policy splits the premium between the broker, the central fund, and the syndicates, and applies a per-claim limit, the remaining aggregate, and the deductible. A claim has one terminal state; a line cannot pay twice. The central fund is a levy-funded, capped, one-shot backstop that requires 2-of-3 signatures; it is not an automatic payer.

The contracts are grouped by object: the root and books; syndicates and lines; brokers; risks; slips; policies; claims; distributions; and the fund. Each object owns its state and exposes a capability rather than an admin API. The reusable pieces are Distribution, Line, and Policy, which R-Share can use for rentals and staged payments.

A mutating operation consumes the object’s state, checks the operation against what it consumed, and posts the new state once. A second operation sees the new state and refuses. That is what makes a subscription sum to 100%, a policy bind once, a claim settle once, and a line pay once. Capabilities are held in contract closures; a caller receives a specific authority, not an admin key.

Lean proves the insurance economics over a shallow state model: capacity, subscription, premium allocation, payable bounds, settlement conservation, exactly-once guards, terminal claim states, and the central fund. In plain terms, it proves the arithmetic and the state machine, not that the deployed contracts implement them, that R-Cash or R-Gen behave as assumed, or that the economics are solvent under real conditions.

On 5 November 2026, the devnet install completed all 17 contracts and the node proposed blocks. The campaign records 37 runs, 375 assertions, and 0 assertion failures. The registered test set has 39 suites: 36 pass and 3 process gates are not run. Coverage is 120 of 145 public arms (82.8%) and 133 of 162 registered arms (82.1%).

The Lean model has 261 theorems, 33 vectors, 51 flow rules, and 11 proved-model core arms across 14 critical primitives. The audit records 25 findings: 22 fixed and 3 accepted boundaries, with 35 hazards and 25 improvements; 30 of 30 concurrency reviews and 42 of 42 composition interfaces are complete. The React/Vite client and the Rust workspace tests pass, and the Playwright journey covers placement through claim settlement.