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 cryptography, distributed systems, and critical infrastructure, 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. One engine across three validated domains: the tactical / DDIL edge, ransomware identity-continuity, and OT / critical infrastructure. Canadian and sovereign by design — runs on Canadian soil or air-gapped, no foreign control plane in the loop.
Explore CairnMachine-Checked CodeInternal tooling
Attestral · 10 languages · 6 formal
Code that carries its own proof — AI-generated functions machine-checked locally (compile, lint, property tests, and formal proof via Kani, CBMC, Lean 4, Dafny, F* and TLA+), auto-revised from the checker's counterexample, then signed with a certificate anyone can re-run offline. Internal tooling I built and run across my own projects — nothing leaves the machine.
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.
Code that carries its own proof
Attestral machine-checks AI-generated code with Kani, CBMC, Lean 4, Dafny, F* and TLA+, auto-revises from the counterexample, and signs a certificate anyone can re-run offline. Internal tooling, same verifiable-systems principle.
See the work →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 →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.