ember arlynx

Resume

ember arlynx

heya@ember.software • github.com/emberian • linkedin.com/in/emberarlynx • lunar.town

summary

software engineer with expertise in formal verification, systems programming, and programming language design. focused on making computers actually work correctly through rigorous mathematical foundations, type systems, and capability-based security. experienced in building critical infrastructure from the ground up, from verified microkernels to zero-knowledge proof systems.

expertise

formal methods & verification: Isabelle/HOL proof engineering, seL4 kernel verification, capability-based security, type system design

systems programming: Rust, OCaml, C, FPGA/HDL (SpinalHDL), compiler implementation, runtime systems & garbage collectors

cryptography & distributed systems: zkSNARKs, consensus protocols (proof-of-stake), blockchain architecture, peer-to-peer networking

developer tooling: documentation systems, cross-compilation infrastructure, build systems, language server protocols

professional experience

this is just an overview of my proudest work. see linkedin for a full history.

founding engineer at O(1) Labs (Mina Protocol)

2018-2021

greenfield development of Mina, the first constant-size blockchain using recursive zkSNARKs:

  • systems-level architecture and implementation in OCaml, maintaining cross-platform native build systems
  • designed and implemented consensus protocol: succinct zk-efficient proof-of-stake with sliding window adapted from Ouroboros
  • networking layer design and implementation (twice over) for peer-to-peer block propagation
  • mentored engineers on protocol details and cryptographic primitives
  • work documented in technical whitepaper

research intern at UNSW / Data61

2016

proof engineering on seL4, the world's first formally verified operating system kernel:

  • substantially overhauled Haskell-to-Isabelle/HOL translator used to generate formal specifications from executable code
  • replaced fragile regex-based rewriting system with proper parser-based approach
  • learned Isabelle/HOL from experts, studied end-to-end correctness proofs (200k lines of proof for 10k lines of C)
  • gained deep understanding of capability-based security and microkernel architecture

software engineering intern at Mozilla

summer 2014

contributed to Rust language during critical push toward 1.0 release:

  • participated in standard library stabilization effort
  • helped establish patterns and practices for production-ready Rust code
  • worked on cross-platform build system and toolchain infrastructure

open source contributions

Rust programming language

2013-2015

major tooling and infrastructure contributions during pre-1.0 era:

  • rustdoc: created the first version of Rust's documentation generator, now fundamental infrastructure used by entire ecosystem
  • target specifications: designed and implemented flexible target specification system enabling rustc cross-compilation to arbitrary platforms via JSON configuration
  • This Week in Rust: started the newsletter that became the primary way the Rust community stays informed about language development
  • VisualRust: initiated Visual Studio integration for Rust on Windows
  • rustc maintenance, standard library contributions, gamedev ecosystem development (gl-rs)
  • maintained development blog documenting the journey

Robigalia

2015-2017

designed Robigalia, a persistent capability operating system built using Rust on seL4:

  • explored intersection of capability-based security and Rust's ownership system
  • designed architecture for orthogonally persistent single-address-space OS
  • investigated how language design enhances operating system security properties

research & projects

see projects for more.

higher order unification research

undergraduate REU

formal methods research on cryptographic protocol analysis:

  • studied higher order unification for intruder analysis in capability-based protocols
  • published paper on cap matching for protocol verification
  • early work that sparked interest in formal methods and capability systems

education

Clarkson University

  • mathematics and computer science (2013-2015)
  • digital art, machine learning, electrical engineering (2022-2023)

UNSW Sydney

  • formal verification and proof engineering (2016)

technical writing

author of technical articles on compiler implementation, type systems, and formal methods:

interests & philosophy

focused on the intersection of programming language theory, formal methods, and systems programming. passionate about:

  • correctness by construction: building systems where bugs are impossible rather than caught after the fact
  • capability-based security: making security properties explicit, compositional, and statically verifiable
  • type-driven design: leveraging type systems to make illegal states unrepresentable
  • developer experience: infrastructure and tooling that makes complex systems accessible

the unifying goal: making computers actually work reliably through mathematical rigor and thoughtful design.