PROOFS & SPEC

Proved on paper. Running in Gazebo.

The SwUM Technical Specification, version 0.2 of 12 October 2026, is a design freeze candidate. Every theorem, bound and wire constant has a numerical check, and all thirty-three pass. An early prototype already runs in Gazebo simulations, where simulated robots split a goal into jobs and coordinate with no central server.

33/33

NUMERICAL CHECKS PASSING

PROVED RESULTS

REPOSITORIES, ONE-WAY DEPENDENCIES

LINES OF PYTHON

Thirteen results. Thirty-three checks. Zero lines of Python.

PROVED

Convergence, spreading time, one start per job, a greedy allocation worth at least half the optimum, leases under clock drift, exact integer inference and an equivariant communication model.

CHECKED

Thirty-three numerical checks cover every theorem, bound and wire constant. They caught a wrong start rule before any code existed.

THE LANGUAGE RULE

Rust first, then C, embedded C and assembly. Training on RUMUS, with Caffe as the fallback. No Python anywhere.

WHAT IS PROVED

Thirteen results, each in one line.

Theorem 1 The shared state converges whatever the order, loss or duplication of frames.

Theorem 2 Worst-case spreading time is (n-1)B, and that bound is tight.

Theorem 3 Over h lossy hops the spreading time has a binomial tail bound.

Theorem 4 With settle time 2D and START dominance, exactly one robot starts each job. 2D is the minimum.

Theorem 5 Bidding converges to the greedy assignment within (K-1)D, worth at least half the optimum.

Lemma 6 A lease length that never expires on a live holder under clock drift.

Proposition 7 Integer inference never overflows and is identical on every robot.

Theorem 8 CommNet is invariant and equivariant under permutations of robots.

Propositions 1, 9 to 13 Address length, symmetric layer dimensions, geometric invariance, beacon and identifier collision bounds, and the bundle Merkle root binding the record list and its length.

WIRE FORMATS

Sized to fit one radio frame.

Frames, records and bundles have byte-level formats sized to fit one IEEE 802.15.4 frame in the common case. The attempt record is 196 bytes. The bundle header is 256 bytes, and its hash is what goes on chain.

Golden vectors come with the specification, so an independent implementation can check its bytes against ours.

REPOSITORIES

Twelve repositories, one-way dependencies.

swum-spec, swum-wire, swum-kern, swum-core, swum-link, swum-models, swum-skills, swum-fw, swum-agent, swum-learn, swum-sim and swum-ops. Each part changes at its own rate and sits on its own side of a trust or hardware boundary.

There are no cycles, and nothing on a robot’s Tier 0 depends on the chain, SNIP or OmniNode crates.

LANGUAGE RULE

Rust first. No Python anywhere.

Rust first, then C, embedded C and assembly. Nothing else is authored in SwUM repositories. Training runs on RUMUS, our Rust framework, with Caffe as the fallback.

Inference on Tier 0 is integer only, so every robot gets the same answer bit for bit.

FOR BUILDERS

What builders get.

The spec Version 0.2, sixteen sections and four appendices, with the check harness that produced every number.

Golden vectors Byte-exact test vectors for every codec, so another implementation can prove it matches.

License MIT or Apache-2.0.

Verify us rpc.sumchain.io, explorer.sumchain.io and github.com/SUM-INNOVATION.

How it works The protocol, the planes, the tiers and the learning loop, in one page.