I founded LambdaClass and Ergodic Group. LambdaClass does protocol engineering, compilers, and formal verification — mostly Rust, Erlang, and Lean. Ergodic Group is the holding company on top: we run software companies, a quant finance operation, an animation studio, a vineyard, and a sushi restaurant, among other things.
I spend most of my time on formal systems, proofs, and verified kernels. I also read too much about uncertainty, fat tails, and the limits of knowledge. The two interests contradict each other and I'm fine with that.
Currently: building stabileo (structural analysis in the browser) and Concrete, a language designed so programs can be proved correct in Lean. Also working on ethrex, lambdaworks, running crash detection signals on centuries of FX data, and building an options backtester.
- ⛓️ ethrex. Ethereum execution client in Rust, both L1 and L2
- 🔮 lambda_ethereum_consensus. Ethereum consensus client in Elixir, built on the BEAM for fault tolerance
- 🔐 lambdaworks. Our SNARK/STARK prover library
- 🏛️ cairo-vm. Cairo VM reimplemented in Rust
- ⚙️ cairo_native. Compiles Cairo Sierra down to MLIR
- 📊 options_portfolio_backtester. Options backtester we use internally
- 🧱 concrete. A language we're building for scalable, verifiable systems
- 🎓 erlings. Erlang exercises, rustlings-style
- 🏗️ stabileo. Open-source 2D & 3D structural analysis in the browser. Direct Stiffness Method, real-time solving, no installation
Quantitative Finance
- 💥 fatcrash. Crash detection using LPPLS, EVT, Hill estimator, VRP, and a bunch of other signals. Rust core with Python/PyO3 bindings
- 💱 forex-centuries. Exchange rate data going back centuries. Useful for volatility research when you don't trust short samples
- 📈 finance_research. Notebooks on options backtesting, tail hedging, carry strategies
Tools
- 📖 readtube. Turns YouTube videos into typeset ebooks
- 🗄️ llm-archive. Ingests all my Claude Code and Codex conversations into SQLite, strips the code, keeps the thinking. Search and analysis over months of LLM usage
- 🏢 holdco. Holding company management — corporate structure, assets, custody, tax
- 🎬 media-server. Self-hosted media server, Docker Compose
- 🧬 DNA. Genetic health analysis pipeline
- 🗣️ stoa. Send the same prompt to multiple LLMs, compare side-by-side. Native app, Rust + GPU
- 📐 Data Science in Julia for Hackers. Open book on applied data science
- ✍️ At the Core of Finance Lies Geometry. In the End, It's All Jensen's Inequality.
- ✍️ The Tail Hedge Debate: Spitznagel Is Right, AQR Is Answering the Wrong Question
- ✍️ Friction as Luxury: What We Lose When AI Gives Us What We Want
- ✍️ Can I Prove Concrete Programs in Lean?
- ✍️ The Death of the Inner Self