I work on a lot of side projects, but not all of them are public or well packaged. Here is a curated list of projects you might find interesting — check out my GitHub for more.
Featured Projects
vfat-rs
A FAT32 filesystem implementation written in Rust. Supports reading and writing files, directories, and long file names.
TLA by Example
Learn TLA+ specifications through interactive examples. Write specs and run the TLC model checker directly in your browser. It has since moved under the official TLA+ org.
tlaplus-formatter
A formatter for TLA+ specifications, based on the Wadler-Lindig pretty-printing algorithm. Now integrated into the official tlatools repository. Read the blog post · Try it online.
Genereto
A static site generator written in Rust. Simple, fast and powerful. It powers my personal website and a few more. Documentation.
Horust
A supervisor / init system written in Rust and designed to run inside containers. Documentation.
You can find more of my projects on my GitHub page.
Notable Contributions
Microsoft SymCrypt — Heap buffer overflow in XMSS^MT signing (GHSA-rvj8-8h6x-hjmg)
Found an integer truncation bug where a 64-bit leaf count was silently truncated to 32 bits, causing a heap buffer overflow during XMSS^MT signature computation. Fixed in v103.11.0. Advisory
TLC Model Checker (TLA⁺) — Concurrency bug in temporal property verification
Identified a soundness bug affecting verification of temporal properties when TLC uses multiple worker threads. Present since ~2009. GitHub issue · Announcement
Maintainer for VSCode TLA⁺ Extension — github.com/tlaplus/vscode-tlaplus
One of the maintainers of the official TLA⁺ extension for Visual Studio Code. Notable features contributed:
- Detect PlusCal/TLA⁺ divergence before translating
- Unicode operator completions
- Integrated tlaplus-formatter support
- Restore counterexample navigation in the MC panel
- Merged stdout/stderr streams to reliably capture SANY output
- Option to keep focus on model buffer when running TLC
- Show errors tab first and add direct links to errors from SANY output
- Colored diff highlighting (additions, deletions, updates) in state changes
- Show simulator progress in the side panel
- PDF generation: feature parity with the TLA⁺ Toolbox
- Display infobox when .cfg file is missing
- Don't generate .cfg file when transpiling PlusCal
- Fix broken syntax highlighting after the first submodule
- Fix commented operator definitions being incorrectly stylized
Other Contributions
TLA⁺ Tools (tlatools) — github.com/tlaplus/tlaplus
- Integrate tlaplus-formatter into tla2tools — ported the formatter to ship as part of tlatools.jar
- Remove RMI dependency from FPSet — enabling CheerpJ compatibility
- Migrate snapshot publishing from OSSRH to Central Publisher Portal
- Print log message when simulator finishes computing initial state
- Fix unreachable branch in Simulator#printBehavior
- Rearrange position of "pc" variable in PlusCal translations
- Update docs about non-deterministic diameter with multiple workers
- Fix bug when
file=argument requires anumargument
Other Projects
TLA+ Wiki
A community wiki for TLA+. Started as a GitHub repository, migrated to DokuWiki, and now hosted at docs.tlapl.us as part of the official TLA+ ecosystem.
Yes, we kana
A webapp to help you learn Japanese: hiragana, katakana and more. I've developed this while studying Japanese.
OpenSingleTab
A simple browser extension to keep your tabs under control. Available on Firefox and Chrome webstores. Open source, safe reimplementation of OneTab.
Apache Oozie Workflow Visualizer
A small tool to visualize Apache Oozie workflows, built while working as a consultant. I was working with very large workflows and hadn't access to any UI.
