Math BSc '26. My thesis formalizes Kalman filtering in the Rocq prover. By day I build tooling that helps certify safety-critical embedded software. Off-keyboard I'm usually into reading and also slowly learning Japanese.

• 🧮 Formal verification: kalman.v, my BSc thesis, the Kalman filter formalized in Rocq, MathComp, Infotheo & CoqEAL. It is largely dedicated to discrete Riccati theory and the algebraic Riccati equation, and written upon Kailath–Sayed–Hassibi's Linear Estimation. The extracted OCaml produces the numerical experiments for the thesis.
• 🛠️ Certifiable embedded (full-time job): I write the tools verification teams run: static analysis and instrumentation of embedded C with LLVM/libclang; statement, decision and MC/DC code coverage; DO-178C / DO-330 tool qualification; air-gapped CI.
• ⚙️ Language & tooling research: Axion, a long-running educational experiment: lexer, parser, C#/Python/Lua emitters. Smaller tools I maintain: plint, a PDF layout linter for frozen-print documents, and rocq-comment-fmt, a comment formatter for Rocq, both in OCaml; vscode-scope-search for search & replace within semantic scopes; typst-djvu for DjVu parsing in Typst (Rust → WASM); textmate.typ, a TextMate grammar converter.
• 🗣️ NLP & ML: ttc library for reading fiction and working out who is speaking: a spaCy pipeline (NER, coreference, span classification), ~80% attribution accuracy. webanno2spacy bridges WebAnno annotations to spaCy, on PyPI. Previously I also did research on Kolmogorov–Arnold networks (KAN) at uni.
• 📟 Systems: I port postmarketOS to phones I have on my shelf: mainline Linux 6.17+ and lk2nd on the ZTE Blade S6, with a new DRM driver for its JDI TD4291 panel; also I do experiments with Hexagon cDSP compute offload on the Redmi Note 9 Pro, patching the FastRPC kernel driver and userspace until signed DSP libraries load outside Android. An old Galaxy A8+ waits its turn.
• 📱 Mobile: storyteller, a Flutter audiobook app with an embedded CPython runtime: the ttc pipeline runs on-device, reading EPUB/FB2/DjVu aloud with per-character voices. Getting spaCy onto a phone took python-for-android recipes for its whole C-extension stack (numpy, blis, thinc…), collected in p4a-recipes.

I write daily
Provers I've used
I've shipped products in
Libraries & infra I constantly use

📈 GitHub statistics