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), Concrete, a language designed so programs can be proved correct in Lean, and lean-extremevaluetheory, a machine-checked library of extreme value theory and heavy tails. Also working on ethrex, lambdaworks, a native compiler backend in Lean, running crash detection signals on centuries of FX data, and building an options backtester.

• ⛓️ ethrex. Ethereum execution client in Rust, both L1 and L2
• 🔐 lambdaworks. Our SNARK/STARK prover library
• 🧱 concrete. A language we're building for scalable, verifiable systems
• 📊 options_portfolio_backtester. Options backtester we use internally
• ⚙️ cairo_native. Compiles Cairo Sierra down to MLIR
• 🏛️ cairo-vm. Cairo VM reimplemented in Rust, now maintained by StarkWare
• 🔮 lambda_ethereum_consensus. Ethereum consensus client in Elixir, built on the BEAM for fault tolerance
• 🏗️ stabileo. Open-source 2D & 3D structural analysis in the browser. Direct Stiffness Method, real-time solving, no installation
• 🎓 erlings. Erlang exercises, rustlings-style

Formal Verification

• 📉 lean-extremevaluetheory. Extreme value theory and heavy-tailed probability in Lean 4: Fisher–Tippett–Gnedenko, regular variation, Karamata, Breiman. ~94k lines, 3,900 theorems, no sorry
• 🛠️ lean-compiler-backend. Native compiler backend written in Lean 4, starting as a QBE 1.3 port. Builds and runs real C programs through cproc
• 🔩 lean4-baremetal. Lean 4 on bare-metal RISC-V, no OS and no libc. Verified SHA-256, a CAN 2.0 parser, and an automotive torque-enable gate, 167 theorems over the code that actually runs
• 🪤 verified-still-broken. Five Lean proofs that type-check and still sit on real bugs. The bug lives in the spec, the model, or the trusted base

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
• 🎬 media-server. Self-hosted media server, Docker Compose
• 🗣️ stoa. Send the same prompt to multiple LLMs, compare side-by-side. Native app, Rust + GPU

• 🦀 Cryptography in Rust for Hackers. From the math foundations up to SNARKs and STARKs, with Rust implementations
• 🤝 Distributed Consensus in Rust for Hackers. Consensus from crash fault tolerance to Byzantine protocols and modern blockchain consensus
• 🔏 Practical Cryptography and Distributed Ledgers. Study guide to cryptography and ZK proving systems, with Pablo Deymonnaz and Diego Kingston
• 📐 Data Science in Julia for Hackers. Open book on applied data science

I keep curated reading lists for whatever I'm trying to learn.

• 🐚 spawnedshelter. The best articles, talks, and books for learning Erlang and Elixir
• 🎲 the_bayes_way. Bayesian statistics
• 🐘 learning_leptokurtic. Fat tails and kurtosis
• 🔁 learning_ergodicity_economics. Ergodicity economics lecture notes
• 💹 learning_economics. Economics books, papers, and courses

• ✍️ A Proof Is Only as Good as Its Spec
• ✍️ 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

X · Blog · Email