About
Engineer working across low-latency C++, Rust systems, quantitative finance, and AI/ML. 21 years of experience. École Polytechnique (X1999), University of Tokyo (Scientific Computing, 2004), DASCA Certified Principal Data Scientist.
Previously: APAC Head of Equity Derivatives Quant Strategies at HSBC; Senior / Head Quant at Shinhan Investment Corp. and KB Securities; Senior Acceleration Architect at Maxeler Technologies (FPGA-accelerated Monte Carlo for a tier-one bank platform); Senior Developer on a multi-exchange DMA/HFT options engine at Webb Traders; earlier roles at Standard Chartered, Daiwa Capital Markets, Dexia Credit Local, JP Morgan Chase, Numerix Japan. Currently Lead Engineer at Anzaetek Inc. in Seoul.
Most of what I ship these days is either closed-source fintech work at Anzaetek (Sqetch platform, time_series_base, finance_lab, omega-functions, portfolio optimisation) or the public personal projects below. Blog posts here describe each with a "what I'd claim / what I wouldn't claim" discipline — the code is the source of truth.
Public projects (all WIP-honest):
- Thetis26 — C++20 lock-free / wait-free data structures. Ring buffers (SPSC / MPMC), dense hashmap, skip list, priority queue. Multi-tool formal verification: TLA+, CBMC, SPIN, GenMC, Nidhugg, Lean 4. Cross-platform: x86_64, ARM64, RISC-V 32, ESP32.
- Seal DAO (WIP) — SQL-native L1 in Rust, with post-quantum signatures (ML-DSA-65) and a PQ VRF (ML-DSA + SHA3). Rocq, Lean 4, TLA+, Kani, Miri, cargo-fuzz verification stack. Several components still scaffolded; see the blog post for what's real vs placeholder.
- gpu-backtest (WIP) — Rust backtesting engine with the Aria strategy DSL (bytecode compiler, register-machine VM running on CPU / CUDA / Metal / OpenCL), snapshot+delta LOB reconstruction, DuckDB data layer.
- notbbg — Go real-time market-data terminal. TUI (Bubble Tea) + Electron desktop + React Native phone clients. ~17 feed adapters across CEX (Binance / OKX / Bybit / Bitget / Coinbase / Kraken), DEX (Hyperliquid / Jupiter / Raydium / Uniswap), macro (CoinGecko / Yahoo / FRED / mempool), news (RSS). Optional PQC-wrapped TLS to a remote collector.
- rust-secure-memory — Rust port of Go's memguard. mlock, guard pages, XChaCha20-Poly1305 enclaves, ML-KEM-768 KEM. Kani harnesses + Lean 4 proofs. Includes
sedit, an encrypted TUI text editor. - fpga-meta-compiler (WIP) — Aria-HDL, a DSL compiling to Verilog / VHDL / Verilator / SVA + SymbiYosys / Lean 4 / CUDA / Metal / OpenCL / resource JSON. Leiserson-Saxe retiming, CDC hard-errors. Several features still thin; see the blog posts.
- numerical-algorithms (WIP) — LU (Doolittle) and QR (Modified Gram-Schmidt) each implemented twice: Lean 4 (ℚ + Float) and F* (fraction-free integer, Z3-verified). Triangularity of output factors proved; full correctness statements still axiomatised + fuzzed.
Blog: see the post list — recent entries cover all the projects above, plus 2020-2025 retrospective posts on earlier private work (Atlas on AWS Braket, Aegis event log, Sensor-Stream-Pipe contributions, QuetzalcoatlProto quantum R&D, Sibelius pricing library, Thetis v1).
Publication: Some usages of functional programming for FO and quants, CUFP 2014.
Links:
Contact: renoir42@renoir42.com