Hi, I'm Federico
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 also work on the core of Ethereum, applied cryptography and cybersecurity.
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.
Built at LambdaClass
- ⛓️ 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
Personal Projects
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
Book
- 📐 Data Science in Julia for Hackers. Open book on applied data science
Writing
- ✍️ 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