OFFLINE COUNTERS AND LISTS, RUST CORE.

Offline edits.
Shared results.

Build apps that keep counting and updating lists without a connection. Your app sends changes when devices reconnect; SafeMesh combines them. Your app supplies the connection and storage.

Start with Rust Try failure modes ↗

Build from source, no Lean setup required

Rust, TypeScript/WASM, Python, C
Compare language capabilities →

Rust, G-CounterTwo writers

use safemesh_crdt::GCounter;

fn main() {
    let mut a = GCounter::new(2);
    let mut b = GCounter::new(2);

    // Each writer reports its own total.
    a.try_apply_bump(0, 2).unwrap();
    b.try_apply_bump(1, 3).unwrap();

    a.try_merge(&b).unwrap();
    assert_eq!(a.value(), 5);
}

Enable JavaScript to run the Rust core via WASM.

Lean proves merge models. Rust is tested against generated cases.
Bindings, storage and transport sit outside those proofs.

Guarantees & limits →

What it does

Build a field inspection checklist that records answers on two devices without a signal, then exchanges both answers for review after a connection returns. Fieldcheck shows this with a Rust application. You can also build a shared member list that accepts edits while devices are apart, or count received units at a clinic and a warehouse; the two-app inventory demo shows that count. The count is for units received, not units left in stock.

SafeMesh supplies the rules for combining those changes. It does not supply the connection between devices, your data layout, or sign-in and access control. A merge combines changes from separate copies. A replica is one device’s copy of the data. A CRDT is a data type whose copies can accept separate edits and merge under a defined rule. See how the rules work. This page follows main (unreleased), rather than a release manual.

Get a result

Follow Get started to save an edit, restart and sync a second replica in a complete Rust or TypeScript program, from main (unreleased) source you build yourself — no Lean build needed. Its stdout is checked by the existing documentation CI job, so what you see is what the fixture actually prints.

Prefer to see failure handling first? Build and run the Rust break-it walkthrough to partition, drop, duplicate and reorder messages between replicas, then heal with anti-entropy and finish with CONVERGED=true.

Build your integration

Choose a Rust API layer by the storage and identity responsibilities you want it to own — raw carriers, a caller-managed event log, or the Linux durable adapter — or call SafeMesh from C ABI, WASM/TypeScript or Python. Use SafeMesh in your code maps each language surface to its ownership contract. For how the layers relate to the proof, see the architecture guide.

Evaluate the fit

SafeMesh’s guarantees are conditional — on delivery eventually happening, on the storage and platform assumptions your integration makes — and its v0 type selection is a separate question from its proof status. Compare the limits against your requirements before committing.

The proof bridges to code in three steps:

LeanModel
Merge is proved to be a join: commutative, associative and idempotent, for the five Lean-backed carriers.
Read the proof and its boundary →
CorpusGenerated oracle
Compiled Lean definitions emit a finite, generated set of expected results — evidence, not production code.
See how the corpus is generated →
RustDifferential test
Rust is checked against that corpus. Bindings, storage and transport are TESTED engineering, not a Lean proof.
Read the claims ceiling →

Pick a data type

Choose by what a value must do when people edit it on separate devices. The G-Counter only goes up; the PN-Counter goes up and down. The G-Set only adds items and never removes them; the OR-Set adds and removes items. Each OR-Set addition needs a fresh token, a unique marker for that addition. If one device removes an item while another adds it at the same time, the new add survives after a merge.

Type	In plain words and an everyday example	Cannot do
G-Counter	A total that only rises, such as units received at two warehouses.	Subtract units or show current stock by itself.
OR-Set	A shared list whose items can be added and removed, such as a team member list.	Make a removal win over a simultaneous new add.
G-Set	A shared list that only grows, such as IDs of visits already logged.	Remove an ID.
PN-Counter	A total that can rise or fall, such as the net change in one stock item.	Prevent two offline removals from overselling.
RGA/Text	An ordered list of entries, such as steps in a checklist.	Move an entry as one built-in operation; the caller supplies positions.
LWW Register	One value where the chosen timestamp decides which edit remains, such as a room label.	Preserve two competing labels.
Enable-wins Flag	An on/off value where a new simultaneous switch-on stays on, such as an alert toggle.	Make a simultaneous switch-off win.
LWW Map	Named values where timestamps decide each name’s value, such as room names keyed by room ID.	Add competing numeric edits together.

The last six types in this list are Experimental in the v0 table below. The concepts guide gives the precise merge rules for the five Lean-backed types. Limits explains where these choices do not fit.

v0 focus

G-Counter and OR-Set are the two types selected for v0; v0 focus in the table means this type selection, within the language-path limits below. All other carriers remain experimental. The repository’s source history records the decision behind this selection; release status is a separate question from proof status, below.

Main is unreleased. Release artifacts and measured platforms are separate from this selection; the install matrix records their availability and evidence. Maintainer support is UNKNOWN for all four language surfaces: this selection establishes no maintenance commitment. Proof breadth and release support are separate: the five existing carrier proofs remain valid.

Type	v0 status	Evidence
G-Counter (`GCounter`)	v0 focus	Lean model, Rust conformance
OR-Set (`OrSet`)	v0 focus	Lean model, Rust conformance
G-Set (`GSet`)	Experimental	Proof and finite-test boundary
PN-Counter (`PnCounter`)	Experimental	Proof and finite-test boundary
RGA/Text (`Rga`)	Experimental	Proof and finite-test boundary
LWW Register (`LwwRegister`)	Experimental	Tested, not proven
Enable-wins Flag (`EnableWinsFlag`)	Experimental	Tested, not proven
LWW Map (`LwwMap`)	Experimental	Tested, not proven

These language paths have different limits:

Rust: G-Counter and numeric/UTF-8 OR-Set mutation, record exchange and checked restore; only Linux Rust has the durable writer.
TypeScript/WASM SafeMeshOrSet: numeric add, applyRemove, contains, elements, merge, observedTokens, and tombstones.
TypeScript/WASM SafeMeshStringOrSetReplica: UTF-8 createAllocated, appendAllocatedAdd, exportIdentity, importIdentity, appendAdd, appendRemoveObserved, mergeRecordBytes, mergeLogBytes, logBytes, versionFor, versionVector, recordIds, sinceLogBytes, elements, observedTokens, tombstones, addEntries, and inspectRecordBytes.
Python: G-Counter mutation/exchange with caller-owned storage; numeric OR-Set mutation/remove/whole-state merge; UTF-8 StringOrSetReplica add/remove, record/log exchange, read/inspect, and caller-persisted identity export/import. No disk I/O or cross-process writer fencing is supplied by that replica.
C: G-Counter carrier mutation/read and delta encoding, and numeric OR-Set mutation/remove/whole-state merge; no log or recovery promise.

The install matrix records measured environments and artifact availability separately. For decrementing stock, use paired v0-focus G-Counters. Application schemas, custom durable replicas and delivery/retry/storage remain caller-owned.

More entry points

Merge illustrations: independent edits, delivery and repeated state.
Project entrypoint: the repository’s current status and package instructions.
Generated API reference: the Rust core API from this build’s source.

Use this site

Site search covers all guides and the generated Rust reference, including source pages; it does not index the contents of linked GitHub documents. Rustdoc provides a separate item search for Rust items. The Lab entry opens the Lab at the address chosen when this documentation site is built; the hosted site includes the Lab under its own lab/ path.

Offline edits.Shared results.