A happy member of the Erlang, ML and Lisp Evangelism Strikeforce. Network protocol RFC fanatic. Distributed systems, data science and finance.

I founded LambdaClass and Ergodic Group. At LambdaClass we build compilers, Ethereum infrastructure, and cryptographic proving systems, mostly in Rust, Erlang, and Lean. Ergodic Group brings together our work in software, finance, and culture, including an animation studio, a vineyard, and a sushi restaurant.

I spend much 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 Concrete, working on the solver behind Stabileo, and formalizing extreme value theory in Lean.

Buenos Aires & Barcelona · Website · Email

• ⛓️ ethrex. Ethereum execution client in Rust, both L1 and L2
• 🔐 lambdaworks. Our SNARK/STARK prover library
• 🧱 Concrete. Experimental systems language with explicit ownership and capabilities, and Lean-checked proofs for supported code
• 📊 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. Structural analysis in the browser, with a Rust solver compiled to WebAssembly. I lead the solver work. Try it
• 🎓 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
• 🛠️ 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
• 🪤 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. Research toolkit for tail risk, bubble signals, and market regimes. Rust core with Python 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

• 🦀 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.
• ✍️ Friction as Luxury: What We Lose When AI Gives Us What We Want
• ✍️ Can I Prove Concrete Programs in Lean?

All writing and interactive simulations

X · Blog · Email