How We Let a Stranger Check Our Consensus Math
Within that scope, the consensus-safety claim underneath it doesn't have to be taken on trust. It can be checked, and on 2026-07-14 it already was: someone who does not work for Solidus cloned the protocol repository, ran one command, and got the same answer the project's own logs show.
That reproduction, and the exhaustive model check behind the design it's testing, are the subject of this page. Both are runnable or readable by anyone, no account, no waitlist, no cooperation from Solidus required.
Run it yourself
The command a stranger already ran, verbatim, from a clean clone of the public protocol repository:
cargo test -p solidus-exec --release --test twolane_vs_oracle randomized
Their result:
test result: ok. 1 passed; 0 failed
1,344 transactions across 3 streams and 40 blocks, zero divergence, about 1m09s to compile. No account was created, no configuration shared, no help given, a fresh checkout and a single cargo test invocation.
This is the low-friction path if the claim below is worth two minutes of a reader's own time. It requires the Rust toolchain and the public repository; nothing else.
What the test actually checks
twolane_vs_oracle is a differential test. It runs two independent execution paths against the same transactions and compares their outputs, a fast lane and a reference oracle, checked against each other block by block. "Zero divergence" means the two paths agreed on every transaction they both processed, for the entire run.
That is worth stating precisely, because it is easy to overstate. Agreement between two implementations on one machine, across one randomized run, establishes that those two code paths didn't disagree this time: it is not a formal guarantee that no bug exists anywhere in either path, and it is not evidence about behavior under conditions the run didn't exercise. It is exactly what a differential test is good for: a cheap, repeatable check that two things meant to compute the same answer actually do, one that any reader can rerun with a different seed and get their own independent result.
The project's own larger run, from the same test harness, processed 2,186,046 transactions across 1,000 streams and 100 blocks, also zero divergence. The stranger's reproduction used a smaller randomized seed set, which is why the numbers differ; both runs are read from the same public logs (differential-large.txt), and both are the same kind of evidence at different scale.
The TLA+ bounded model check
CORRECTION, 2026-08-02: this section previously said "the HotStuff-derived consensus core has a formal specification in TLA+", which a reader would fairly take to mean the consensus this network runs. It does not. There is exactly one TLA+ file in the repository, and its own header says it specifies the two-chain, consecutive-view commit rule of the v2 core, mirroring that crate's safety and core modules. The chain running today uses the older three-chain implementation, and no specification covers it. The model check below is real, and it covers an implementation that is not deployed. Everything else in this section stands as written.
Separately from the differential test, the v2 consensus core has a formal specification in TLA+, checked with TLC. The published result: 963,033 states checked exhaustively at MaxView=2, zero safety violations. A larger, non-exhaustive simulated run at MaxView=4 covered 124.4 million states, also with zero safety violations found.
Call this precisely what it is: a bounded model check, not a proof. MaxView=2 fixes the number of consensus rounds the exhaustive search considers; every reachable state within that bound was enumerated and checked against the safety property, and none violated it. That is a strong result: it is not the same claim as a proof that the protocol is safe at every view number, under every schedule, forever. The distinction matters enough that this page states it every time the check comes up: bounded model check, never proof.
The specification and the full results file (tla+/TLC_RESULTS.md) live in the public repository alongside the code they model, which is the v2 crate rather than the deployed one. Reading it is a heavier lift than running the differential test, reproducing the exhaustive check yourself means installing TLC and running it against the spec, but the results file is there to be read and the spec is there to be checked against the implementation it claims to describe.
Reading the throughput number honestly
The differential-large log that produced the 2,186,046-transaction run also produces a throughput figure in passing, because the test happens to report one. Any throughput number from that log, or from the project's other benchmark logs, was measured on a single Apple M4, 10 cores, one machine, never a distributed network, never multiple validators under load. That caveat travels with the number every time it's mentioned here, because a single-machine figure and a network's real throughput answer different questions, and blurring them would misrepresent what was actually measured. No geo-distributed or multi-node figure exists to cite instead.
What this checks, and what it doesn't
Put together, the two artifacts on this page answer a narrower question than "is Solidus's consensus correct." They answer: does the fast execution path agree with a reference implementation across a large randomized sample, and does the consensus core's formal model hold up under exhaustive search within a bounded number of rounds. Both answers are yes, both are independently checkable, and one of them has already been independently checked by someone with no stake in the outcome.
They do not answer whether the design holds at production scale, under adversarial network conditions, or across an unbounded number of views: those are different, harder questions, and this page isn't claiming otherwise.
Why this is the right thing to check first
For a reader deciding whether the consensus design is sound enough to be worth operating at all, before any yield exists to operate it for: this is a smaller, more answerable question than "should I trust this project." It doesn't require trusting anyone. The differential test and the TLA+ specification are both in the public repository; the differential test is runnable directly, and the specification is readable and checkable against the code it describes without asking Solidus for anything. That's the point of publishing both this way rather than as a claim in a document: a reader who wants to verify the consensus math can do it without an account, without permission, and without taking the project's word for the result.
Where the rest of this lives
If a reader arrived here from a technical write-up on another platform, a dev.to post or a forum thread describing this reproduction: this page is the place the full detail and the exact commands live going forward. It isn't a rewrite of that material; it's the canonical, indexable home for it, kept current as the repository changes. For the broader question of whether anything on this site can be taken at face value at all, see the shipped-vs-roadmap page; for what the consensus engine underneath is actually verifying identity for, see the Proof-of-Identity page.
Terms used above with precise technical meanings, BFT and finality, are defined at length in the lexicon; this page uses them only as needed to explain the differential test.