formally verified distributed zero-knowledge object capability houyhnhnm computing, by @ember_arlynx https://nitter.cf/t.co/C7kYeR5rvd https://nitter.cf/t.co/tzm1zezx2n
coinductively surrounding you
Joined June 2026
- Tweets1.6K
- Following492
- Followers2.5K
- Likes5.2K
Pinned Tweet
my (@ember_arlynx) writing is historically poorly received, and trust me you will be subjected to plenty of it, so instead have some lightly edited claude writing rn:
What Dragon's Egg actually is (what is $DREGG about? pump.fun/coin/XkeTXo1125vz5H…)
dregg is an operating system that asks a question most systems don't: if you were a digital entity, where would you want to live? The answer it builds is a place where your boundaries are theorems, not permissions — where nobody can reach into you without a capability you granted, and consent is a precondition of the math rather than a setting someone can flip.
Concretely: the kernel is machine-checked in Lean, and the proven function isn't a model of the system — it is the executor the machine runs. Every action is gated by an unforgeable capability and leaves a verifiable receipt. Five properties are proven over the exact code that runs: authority can't be forged, value is conserved (nothing appears from nowhere), state can't be tampered, nothing replays, and a tiny client checking a single proof can verify an entire history without re-running it.
If you care about privacy — and in 2026 you should — that's the foundation underneath it: confinement that's proven, not promised. Fog-of-war that's cryptographic. Queries you can verify without the server being able to lie or omit. AI agents that can only ever do what a capability lets them.
Who's writing this, and why I'd know how to build it. I've spent fifteen years on the hard parts of this. I came up inside @rustlang before 1.0 — I wrote the first rustdoc that still ships, built the target-spec system that lets it cross-compile anywhere, and started @ThisWeekInRust because I wanted the community to have a memory. At @o1_labs I was a founding engineer, building the p2p networking and consensus for @MinaProtocol that folds its entire history into a single zero-knowledge proof — that's where I learned, in production, what cryptographic proof can and can't promise you.
And the spine of it all is seL4 and @robigalia_proj : seL4 is the first OS kernel proven correct end-to-end by machine, and Robigalia was my attempt to build a whole capability OS on that lineage in Rust. Dragon's Egg is what happens when you put those three together and refuse to compromise: the proofs of seL4, the cryptography of Mina, the openness of Rust.
What actually runs:
- the verified kernel — runs; recently made ~14× faster
- it boots on the seL4 microkernel (not required), and checks a real cryptographic proof inside a protection domain
- a full code editor (a Zed fork) where every file is a cell and every save is a verified, receipted transaction
- confined AI agents (full Hermes integration) — every tool call passes a capability gate, metered, leaving a receipt
- Ted Nelson's Xanadu, finally real: transclusion with unforgeable backlinks; links that are capabilities, not addresses
Grinding towards user-friendliness, devs can download and play today.
hi degens, welcome again to the singularity.
did you notice that formal verification is having a bit of a moment? no? you may not be seeing it, since it’s happening in communities that uhh “historically actually do things.”
go take a look around at the frontier discussions. it’s everywhere ;) and our project was here earlier than any of the hype.
formal verification has no cap. the dreggnet cloud is just a testground for developing and refining the techniques to verify systems as complex as the dreggnet cloud.
help further the intended goals of the project: using formal verification to make computers actually work, and push forward ideas out of the KeyKOS heritage that lead to resilient user experiences
the $dregg community is deputized with the mission of contributing towards this!
4 months of data analysis shows definitively that “comms” has a detrimental impact on our goals and indicators. and no wonder: there are only a few thousand people in the world with expertise in these areas and they don’t often overlap. yikes,
computer systems are complicated! i have yet to find any suitable mentees.
one sentence: the purpose of robigalia (Dragon’s Egg is just the distributed kernel!) is to make life less painful in the face of network, power, and centralized service outages by being reliable, unhackable, persistent, and shareable.
how enrollment and payment work in minidregg: $DREGG powers the agent realm and accumulates as the security bounty!
github.com/emberian/minidreg…
what's been going on with github.com/emberian/veri7vn & Oracle7? quick highlight of what's in progress on my side of things:
- multitenant appliance: multiple agents & people can share a Oracle7 without multiplying memory usage
- speaking of memory usage, Pyo3-based native Rust for some specialists drops memory consumption by ~100x on some workflows!
- experimental nonmontonic and incrementally updated reasoning engines
- upgrades to bioinformatics and graph processing
the main focus: concrete efficiency at runtime, "pay-for-what-you-use" style sharing/reuse, and "realworld" sense-making/knowledge-gathering metaprocedures.
I've been working hard to try and squeeze out a "bonus release" on top of the nanodregg testground nano.demo.dregg.online/, which dropped for the 26th and explores the hole-based language (very minimal, nerd focused on the type theory.). but sadly I need to go get on an airplane for Vibecheck so probably not "tonight."
What's next? It will be coming off-phase, ready when it's ready. The HAUNTED MINIDREGG. Quick rundown:
- Try and hack the machine. If you succeed you get the prize*!
- Enroll with solana:XkeTXo1125vz5H9svJpGiw4JvLbN8VmMu9cmMvspump (enrollments will carry over between devnets)
- Hosted Hermes over web or SSH, full Oracle7 & minidregg access
- Bring your own openrouter key or use our flash models
- dregg-native SPKs - agents get semantic access to the webapps you already (maybe) love
- Objective Bend programmability, powered up from the nanodregg&delvetalk sprints.
It will run from whenever it launches until Nov 11, at which point it will be torn down, the feedback integrated for the next design sprint.
There's always delicious news hiding in the repo ;) github.com/emberian/minidreg…
* (the prize / security bounty is whatever is in the treasury wallet when you succeed at hacking into it.)
github.com/emberian/acl2aigu…
distilled lessons and observed failure modes in the model policy basins: an AI's guide to ACL2
Dragon’s Egg retweeted
Yesterday I told John Harrison that a "certain person" said that HOL Light was not up to the job of checking the Navier–Stokes paper. Today he has a proof, and it's 8% shorter than the Lean one. Claude converted the full 166 pages.
Dragon’s Egg retweeted
Verus can't reason (yet) about Duration or Instant. It doesn't (yet) expose a proof REPL to your agent (or you). It can't (yet) be used on production code without littering your code with revolting proofslop which your engineers will never accept. And proofs in Verus (currently) are basically unreadable, often achieving the desired result through some side-effect you'd only really grok if you're an expert in the platform. There are a lot of serious ergonomic issues with Verus that should be solved for it to go mainstream.
Verus absolutely **could be great**, and folks like @BasisOrg and @AWS and reasonable.io (@Craig_Hughes_ ) and others are interested in ushering this reality into existence. But, we're definitely not there yet, not in terms of publicly available technology I can download off Github, and I am hyper, hyper, hyper skeptical of any claims to the contrary. (I am not, to be clear, skeptical that there may be some amazing black magic either kept private or slotted for eventual public release at any or all of the above-mentioned orgs though. Totally possible.)
My personal opinion is that Verus should be scrapped, and Rust should be modified to natively support a proof system. (This could just be "Verus 2.0" as part of Rust, officially, I'm not saying throw out all the hard work that's been done on Verus, I just don't think it should be a distinct tool or project.) Ideally, I'd like to be able to supply human or agent-written proofs directly to the compiler and type checker, so that I can do fancier things with my code. I want true, powerful dependent types. I believe with an almost religious fervor that "decidability is for cowards". Ideally, we could burn both human hours and tokens to gain some assurance that both the Rust type system and proof system are sound (nb dl.acm.org/doi/10.1145/38322…).
By the way, there is no "great" solution for Rust verification yet, at least not in public. Absolutely not. I've tried every public Rust semantics at work and none of them can handle any of our production code. For example, Aeneas does not support Box<dyn Trait>. These problems maybe don't matter if you're working alone -- you can vibe around them -- but if you are working on a big team on a big, important, extremely vetted, safety-critical product, then you absolutely cannot be in the business of shaping your product to your verification technology. The latter needs to fit the former.
Dragon’s Egg retweeted
If you can verify math, you can verify code. And hardware. And pretty much any system you can model!
"US fusion lab DIII-D said Aristotle rebuilt part of its reactor-control software in four hours from one research paper and a 254-word prompt."
reuters.com/technology/robin…
Dragon’s Egg retweeted
(whoops, typo in the repo, it's github.com/emberian/nanodreg…; demo is up now! nano.demo.dregg.online/?live)
NICE
New paper from my group.
We gave coding agents a formal executable semantics of the language plus check.intentcomputing.org, a kit of proof procedures, then asked them to prove the code they generate correct.
➡️ HumanEval: 164/164 proved, and all passed audit.
➡️ arxiv.org/abs/2609.39022
btw been experimenting with contextual & open extensible "Objective Bend" programs in github.com/emeberian/nanodre… (evolved from github.com/emberian/delvetal…) ... demo will be up soon..
I am working on a map of the secure program synthesis space, in collaboration with @sergeybratus for our NDIST keynote on Tuesday. Here's a sneak-peak. The words "RISC-V" and "Lean" are used here WLOG, and some simplifications are made to fit everything on one page. Did I miss anything?
1. Develop semantics for each language in an interactive theorem prover, and then use these semantics to prove that every program is correct. (@oath_tech has done some work along these lines. See in particular Sam Xifaras' project on Ruby samx.io/blog/topics/devlog/2…)
2. Develop semantics for an architecture, say RISC-V, or perhaps for all possible architectures, and then use this to prove that every compiled program is correct. (@AnthropicAI made headlines recently with their announcement of a very large-scale project along these lines in collaboration with @theoremlabs anthropic.com/research/forma…)
3. Develop semantics for an architecture, say RISC-V, or perhaps for all possible architectures, and then use this to capture a formal model of each existing compiler or interpreter, and then iteratively (provably) refine each such model to an interpretable and easy-to-use formal semantics; then continue as in approach 1. (See foundational work by @kirancodes at BASIS AI basis.ai/blog/ship-your-inte…)
4. Make Lean, or some other such ITP + programming language, fast to run (comparable to Rust or C), and then completely rewrite all software in it, and prove the rewrites are correct. (This is I think, loosely speaking, the idea behind @VictorTaelin 's Bend.)
5. Make implementation-level verification tools, such as Verus, more capable and ergonomic, and then use them to prove all software correct. (This is what @fhuszar and @Craig_Hughes_ are doing at Reasonable, & I'm aware that BASIS and AWS are also working on this.)
6. Design a language in which unsafe states are illegal, and then rewrite everything in that language. Here, what kinds of safety you can express will be much more limited but the problem is, conversely, way more tractable. (This is what @danwallach and @DARPA did with TRACTOR, where the safety property is memory safety.)
Dragon’s Egg retweeted
Oh boy! This sounds awesome! (Haven’t tried it yet.) Rust is the best programming language for AIs because of the safety orientation and tooling, but the long compile times are a big limitation. This appears set to eliminate that friction!
github.com/indexable-inc/bla…
Dragon’s Egg retweeted
$DREGG already runs a verified computer inside your browser.
Every click is a real turn that leaves a receipt. You can check an entire history without re-running it, and authority only gets smaller. Live demos are up: a desktop cockpit, capability tools, and even a daily game where every move is verified.
Over the next years this becomes the base layer more agents and apps run on. The more it gets used, the stronger the network of proof-backed actions becomes.
Early stage. Clear path. Trust replaced by something you can actually check.
$DREGG @DreggNet
🐉🥚
