start
the first
five minutes.
Everything runs locally from a clean checkout — this repo and cargo are the only requirements. Pick a door.
door A — run a node
The node's state producer is the Lean executor itself. Start one, faucet a cell, read it back — a real turn through the verified kernel, on localhost.
git clone https://github.com/emberian/dregg && cd dregg
cargo build -p dregg-node -p dregg-cli
./target/debug/dregg-node init --data-dir /tmp/my-dregg
./target/debug/dregg-node run --data-dir /tmp/my-dregg --enable-faucet --port 8421 &
curl -s http://localhost:8421/status
# {"healthy":..., "state_producer":"lean", "lean_producer":true, ...}
door B — sign real turns
The CLI manages your keys and drives a full app lifecycle against your node — each step a real signed turn on the verified commit path.
./target/debug/dregg --node-url http://localhost:8421 demo --passphrase pick-one # faucet → register a name → resolve → transfer → revoke — each a verified turn.
door C — the desktop
deos: the native cockpit that embeds the real verified executor. A heavy build — use --release.
cd starbridge-v2 && cargo build --release
who's building this
dregg is a continuation of work I've been at since ~2015 — everything I learned building an OS kernel, a zero-knowledge blockchain, and formally verified software, smashed together.
rust · pre-1.0
Wrote the first version of the shipping rustdoc, specced & built the cross-compilation target system, started This Week in Rust, kicked off VisualRust, cargo-lite, gl-rs.
mina · protocol engineer
At O(1) Labs during Mina's birth — p2p networking, storage, protocol & consensus, build/packaging. A hash-linked proof system that keeps blockchain history constant-size.
seL4 · robigalia
Work on seL4 — the first OS kernel with an end-to-end machine-checked correctness proof — and creator of Robigalia, a persistent capability OS in Rust. dregg's direct lineage.
More at ember.dev. Built with Claude, in agentic swarms.
go deeper
the technical index
The repo's docs are the dense layer: the machine-facing reference, the guides, the file:line-grounded reference set, and the assurance case with its theorem names. start at the README.
the exact guarantees
docs/ASSURANCE.md states the five guarantees as Lean theorems, each with non-vacuity witnesses, each axiom-pinned — plus §3, the honest enumeration of every open seam.
the community
Builders, provers, and the curious: the Discord · @DreggNet for the weekly roadmap posters.