Skip to content
You must be logged in to sponsor emberian

Become a sponsor to emberian

@emberian

emberian

USA

hello! I'm a longtime independent open source software developer. I believe strongly in building and researching in public, and have been doing so continuously for over a decade. some of my early work in the Rust community set standards that are still running to this day (rustdoc, This Week in Rust, xcompile target spec, int/uint->isize/usize, gl-rs (and the bjz ecosystem in general!), etc). my work at O(1) Labs delivered the first zero-knowledge rollup. I worked on the seL4 verification at UNSW. the throughline of all of this is reasoning-forward, verification-first technologies. what is Houyhnhnm computing anyway?).

Blah blah blah: mathematical foundations of Agentic Coordination and scalable software verification.

My research is substantially AI-limited and reasonably token-efficient. I use a mixture of models with coordination powered by cv (clustervision).

Your money will be used push these (and future!) projects forward, and feeds into a virtuous cycle – financial-precarious-banishment makes for a more productive headspace :)

Dragon's Egg is the flagship project organizing my work right now. I'm also assisting with development https://builders.dev and https://wallace.so. I am the CTO of https://simbi.com, a non-profit mutual aid and community organization platform spearheading ongoing operation and development.

as a hobby I'm interested in gamedev. I've made a somewhat novel & engaging board game https://github.com/emberian/automatafl that I am still proud of :)

@emberian

Allow me to work on projects one more day per week

Featured work

  1. emberian/dregg

    Distributed object-capability authorization with ZK proofs

    Lean 31
  2. emberian/svenvs

    A self-verifying, self-improving Place for an AI to live within: an untrusted inhabitant acts through a machine-checked policy envelope whose own verified prover (Candle/HOL Light on CakeML) gates …

    Standard ML 12
  3. emberian/cv

    agents can read each others minds (session logs)

    Rust 7
  4. emberian/clairnets

    GLaDOS — Geometric Lattice Deduction Over Streams: param-efficient sound-reasoning organs (Clifford geometric product + lattice abstract-interpretation + recurrent deduction)

    Python 3
  5. emberian/lean-uwueave

    Machine-checked answers for DAG/tree CRDT builders: the invariant-confluence dichotomy, a proof-carrying composition DSL, and the Rust that follows the theorems. Companion to universal-weave.

    Lean 4
  6. emberian/minidregg

    Condensed & experimental proof systems for zk/fhe and semantics for agent coordination

    Lean

Learn more about sponsoring developers and organizations.

Report abuse

0% towards $750 per month goal

Be the first to sponsor this goal!

Select a tier

$ a month

Choose a custom amount.

$7 a month

Select
  • Get a Sponsor badge on your profile
  • Appreciate seven (7)

$100 a month

Select

$1,000 a month

Select
  • I'll join your company or group chat for advice and support (Rust, formal verification, blockchain, functional programming, whatever!)