DISTRIBUTED SYSTEMS · VERIFIABLE COMPUTING · APPLIED CRYPTOGRAPHY
Most systems ask you to trust the result. I build ones you can verify.
I'm Kyle Clouthier — I build trustworthy, deterministic systems across distributed infrastructure, verifiable computing, and applied cryptography, taking hard problems from applied research all the way to working, adversarially-tested implementations.
Based in Petawawa, Canada. Open to senior / principal engineering and research roles, design partnerships, and funding discussions in distributed systems, trustworthy computing, and applied cryptography.
ONE PRINCIPLE
Every output carries a proof anyone can reproduce.
Where most systems ask for trust, mine hand you a way to check — a byte-for-byte reproducible receipt, a signed and replayable audit trail, a deterministic answer that is identical on every machine. The same idea runs through all of the work below: trust that survives the network failing, computation you can reproduce exactly, and memory you can replay.
VERIFY IT YOURSELF
Engineering discipline you can check
Not claims — evidence you can open and run. bitrep is open source on crates.io, npm and PyPI with its Lean proofs public, and reproduces one hash across four architectures in your browser. The same discipline runs through everything I ship.
bitrep is published on crates.io, npm and PyPI — MIT-licensed, every claim inspectable, install it and check for yourself.
The rounding, merge and binding theorems are machine-checked in Lean 4 — zero sorry, axiom-audited in CI. Cairn adds its own Lean 4 + ProVerif proofs.
bitrep asserts one hash across x86-64, ARM64, Windows and WebAssembly in CI on every commit — reproduce it on your own device.
The Rust bits symbolically model-checked with Kani/CBMC; the Cairn trust protocol verified in ProVerif with the attacker modelled explicitly.
bitrep differentially fuzzed against an independent big-integer oracle — real bugs caught, fixed, and kept as regression records.
bitrep runs the actual Rust verifier compiled to WebAssembly — offline, zero network imports. Reproduce the hash on your own device.
A body of work, one recurring theme
Verifiable, deterministic systems — a trust platform validated across three continents, open-source proofs you can run, and internal tooling built on the same principle.
Reproducible ComputationOpen Source
bitrep · Rust · JS · Python
Order-invariant, bit-identical floating-point reductions — proved in Lean, checked by Kani, one SHA-256 across four architectures in CI on every commit. Shipped for Rust, JavaScript, and Python (crates.io, npm, PyPI). The open work sample: every claim inspectable, and a live demo that runs the proof on your own device.
Overview, demo & sourceDistributed TrustFlagship · under NDA
Cairn
Serverless trust — devices admit and revoke each other offline, with no central server, post-quantum end to end. The deployable application is identity continuity: keep your workforce authenticating and still revoke a compromised device while Okta, Entra or AD is down, with a signed audit of exactly who was admitted during the outage. Hardened where conditions are worst — real NATO mobility data, a drone fleet under jamming. Canadian and sovereign by design.
Explore CairnMachine-Checked CodePublished research
Attestral · 10 languages · 6 formal
Code that carries its own proof — the model proposes, a separate verifier adjudicates, and only a passing check mints an ed25519-signed certificate anyone can re-run offline. Flagship demonstration: the certified anatomy of the 2026 Jacobian Conjecture counterexample — 43 signed certificates, 20 Lean 4 kernel proofs, published with a DOI.
See the workDeterministic Memory
Neruva · internal R&D
A reproducible memory substrate I built and run across my own projects — deterministic recall, provenance, and replay-audited state.
See the workProof, not promises
Real data. Reproducible methodology. Published.
The proof you don't have to trust
An AI helped disprove the 87-year-old Jacobian Conjecture. Attestral certified its entire structural anatomy: 43 signed certificates, 20 Lean 4 kernel proofs — every claim re-verifiable on your own machine.
Read the case study →One SHA-256 across four machines
bitrep reproduces a bit-identical hash across four CPU architectures, in your browser, live — the open-source proof that a result can carry a receipt anyone can check.
Run the proof →Trust that survives the outage
Cairn validated live across Toronto, New York and London over the open internet — admit and revoke with no central server, machine-checked in Lean 4 and ProVerif.
See the validation →PUBLISHED
Peer-checkable, DOI-archived
Five records on Zenodo (CERN) — each with re-runnable artifacts, not just prose.
10.5281/zenodo.21865170
Passing Proofs That Prove Nothing
Vacuity, precondition & completeness for Rust/Kani
Zenodo · 2026
10.5281/zenodo.21567375
Verify-in-the-Loop: Proof-Carrying AI Mathematics
The Jacobian counterexample, certified
Zenodo · 2026
10.5281/zenodo.21420267
Correctly Rounded Least Squares & Influence Receipts
Exact downdating, optimality certificates
Zenodo · 2026
10.5281/zenodo.21420265
Verifiable Pooled Statistics
Signed aggregates, no trusted party
Zenodo · 2026
10.5281/zenodo.21420261
Exact Float Counter CRDTs
Machine-checked convergence
Zenodo · 2026
What I work in
Four lanes, one throughline — applied research taken to working, tested implementations.
Distributed systems & infrastructure
Serverless / offline trust meshes, consensus-free replication, partition tolerance, zero-trust identity, CRDTs — adversarially red-teamed.
Verifiable computation & provenance
Bit-identical reductions (bitrep), machine-checked code with signed certificates (Attestral), hash-chained receipts, replayable audit, formal methods (Lean 4, ProVerif).
Numerical analysis & HPC
Exact arithmetic, error-free transformations, GPU kernels, bit-reproducible compute.
Applied cryptography / PQC
Post-quantum signatures (ML-DSA / FIPS 204), hybrid trust anchors, key exchange, threat modeling.
Why I build this — FavourBee
Built on the same Sybil-resistance principles as Cairn, FavourBee is a free mutual-aid network I built and shipped end-to-end — a live, full-stack, bilingual platform with a tested trust graph. It's the reason the rest of this work exists: proof that verifiable trust can help real people, not just enterprises.
Let's build something verifiable.
Senior / principal roles, research collaborations, design partnerships — and, for Cairn, evaluations and funding discussions under NDA.