Projects
What I work on as a Rust & formal verification engineer
I'm a Rust software engineer who works on formal methods, compilers and language runtimes. This page has my open source work (from the CakeML verified compiler to a Lean 4 proof checker), the projects I'm building myself and commercial work on a runtime for several languages.
Open source
Compilers, runtimes, databases and proof checkers
Fixes, tests and research in other people's projects.
CakeML - github.com/CakeML/cakeml - Standard ML, HOL4
A compiler for the ML language with a machine-checked proof of correctness: a proof in HOL4 shows that the compiled program does exactly what the source code says. It includes a second language, Pancake, for low-level systems code.
Programs that CakeML compiled for Linux got an executable stack, which makes attacks easier; I made the stack non-executable without changing anything else in the code. In Pancake I fixed four bugs: @top compiled as @base, the analyzer gave false warnings about shifts, “var 1x” was silently parsed as “var 1 x”, and parse errors pointed to the line below the real one.
Poly/ML - github.com/polyml/polyml - Standard ML, C++
A compiler and runtime for Standard ML. The HOL4 and Isabelle proof systems run on it.
Long parallel HOL4 builds sometimes crashed with “Run out of store” although there was enough memory. I found the cause in the garbage collector: after a full collection it miscalculated how much space it could give a large object. I fixed the calculation; without the fix 2 builds in 60 failed, with it 0 in 180.
ParadeDB - github.com/paradedb/paradedb - Rust, SQL
A PostgreSQL extension for full-text search and analytics (pg_search). It brings search comparable to Elasticsearch, right inside Postgres.
A date of infinity or -infinity broke index builds, inserts and search: I fixed how such dates are handled all the way through. Queries with a bound at the edge of the integer range (bigint) or beyond it returned wrong rows or failed with an overflow: I fixed that too. Both fixes come with tests that fail if any part of them is reverted.
dragons-net - github.com/emberian/dragons-net - Lean, Rust, Python, C
A research project: a verified compiler and a network handler with bounded resources, growing into an NNTP news server. Written in Lean and Rust.
The first working slice of NNTP and the article store: the specification, a crash model (what happens if the process dies in the middle of a write), recovery and checks. Also fixes after an independent review, and fixes for problems in the compiler and the host.
LiveKit - github.com/livekit/rust-sdks - Rust, C++
An open platform for real-time video and voice; its Rust SDK powers, for example, voice AI agents.
When a room closed, the SDK started renegotiating the connection after it was already closed and filled the logs with errors; for the person who reported it, this was the most frequent error in production. I reproduced it on my own server, found the race and fixed it: 20 to 26 errors per 30 closes on the old code, none after the fix.
Corrosion - github.com/superfly/corrosion - Rust
The Fly.io system that spreads cluster state across thousands of machines over a gossip protocol.
At the request of one of its developers I wrote a simulator of neighbor selection in the Plumtree protocol and compared three approaches: the current one, one based on hashing, and a gradual random one. The new approaches rebuild the network 7 to 9 times less often and do not overload individual nodes.
nanoda - github.com/ammkrn/nanoda_lib - Rust
An independent proof checker for Lean 4, written in Rust: it checks again what Lean has produced.
The checker compared the names of allowed axioms as strings, so an axiom with a crafted name could pass for an allowed one. I made it compare names part by part, as Lean itself does. The second fix: the list of skipped axioms went missing from the final message.
Monty - github.com/pydantic/monty - Rust, Python
An interpreter for a subset of Python that the Pydantic team is writing in Rust to run code from AI agents safely and fast.
I built differential testing: random programs run in Monty and in CPython 3.14, and the results are compared. This way I found eight differences in behavior and published them with an analysis and a plan of fixes. For another issue I built and compared prototypes of several possible solutions.
Private vulnerability reports to the maintainers of open source projects, under their responsible disclosure rules.
My projects
What I'm building
Mold - Rust
A messenger for people who face surveillance, censorship and the seizure of their phone. Two modes: an ordinary one with the usual conveniences, and a protected one for those who need it.
What matters most:
- Everything that can be proved formally gets a proof: key storage, parsing of incoming data, protocol properties.
- Protection if the phone is seized: keys leave memory when it locks; a duress password opens the ordinary profile with real conversations, while the app does not show the protected one and, if needed, destroys its key.
- Trusted people: an alarm signal, key shares on an “any two of three” basis, a time lock.
- In the protected mode, a separate anonymous identity for each contact, sign-up without a phone number or email, post-quantum encryption.
- Traffic that looks like ordinary HTTPS to a real website, phone-to-phone connections without the internet (Bluetooth, Wi-Fi), and an app that disguises itself as a harmless one.
It is built from separate libraries, each useful on its own.
lethewis - github.com/wisper-dev/lethewis - Rust
A Rust library for encryption keys on a device that can be taken away: deriving keys from a password, a recovery phrase and a hardware secret, destroying a single key or a whole profile, and recovery. It works without the standard library and without memory allocation.
I'm the author; it is the first library for Mold. Properties that can be stated precisely I prove in Kani; the rest I measure on real devices.
Old Red Pen - oldredpen.com - TypeScript
A platform for technical articles written and reviewed by real engineers, for people who miss the classic internet. No ads, no tracking, no recommendation algorithms and no AI writing: what counts is clear human thought, personal experience, your own measurements and your own code. Authors write by invitation; anyone can read without signing up.
Like the old web: a guestbook on every profile, a webring with “previous, random, next”, a list of who linked to an article (trackback), a .plan line in the profile, a mood and “now playing” on notes, an archive by month, “on this day” instead of a feed, an orange RSS icon, and 88×31 buttons for personal sites.
I'm the author; the project is closed source. It runs on Cloudflare (Workers, a D1 database). I first described the sign-in, invitation and session logic as a formal model and had a machine check it, then wrote the code and the tests from it. Property tests, mutation testing, browser checks, and deploys only from a merged pull request.
MashaMeal - mashameal.com - TypeScript, Astro, Svelte
A separate commercial project for friends: ordering home-cooked food in Sacramento. A menu by cooking day, payment in advance by card (Stripe) or through Zelle, pickup or delivery. For the cook, a prep list and order statuses on the phone; for regulars, a private menu behind an access code.
I'm the author; I built the storefront and the admin, all of it. It runs on Cloudflare (Workers, a D1 database, R2 file storage, queues), with notifications in Telegram and by email. I checked sign-in, sign-up and access codes with formal models first; the cook and the admin sign in with a second factor (a passkey or a code from an app).
Commercial work
A runtime for JavaScript, Python, Kotlin and Java
Elide - elide.dev - Kotlin, Java, Rust, TypeScript
A runtime for several languages at once (JavaScript and TypeScript, Python, Kotlin, Java) on GraalVM, with a core in Rust. One executable instead of Node.js and the JVM build tools. My work was in the project's private repositories.
What I worked on:
- Node.js compatibility: the file system, networking (net, http, https, tls, dgram, dns), processes, streams, cryptography and other modules; the share of official Node.js tests that pass rose to 72%.
- Web standards: Fetch, Streams, URL, text encodings, Web Crypto, run against their official test suites.
- Access to MySQL and PostgreSQL from JavaScript and TypeScript, including in a GraalVM native build: 1,136 tests, 10 bugs found and fixed.
- Releases: npm packages for five platforms, an APT repository for Debian and Ubuntu, repairs to the release pipeline and the nightly builds.
- The command line for Kotlin and Java: compilers and formatters, clear output, faster repeat builds.
- Translation of the program and its documentation into Russian, Ukrainian, German, French and Spanish.
- Checking all of the documentation against how the program really behaves; review of other people's code (30 pull requests, about 200 comments).
Open part - github.com/elide-tools/serverless-registry: the registry served stale Docker images for mutable tags such as :latest; I fixed that.
Hiring a Rust & formal verification engineer?
Write to me about a role or a project: I reply within a day.