Series · Concrete
A Fact-Producing Compiler
Concrete already reports facts about authority, allocation, recursion, loop boundedness, trust, fingerprints, and proof evidence. The next step is making those facts queryable.
Federico Carrone
I grew up in Argentina, where you learn early that money breaks, institutions fail, and the systems people depend on are more fragile than anyone admits. That shaped everything I build now.
Through LambdaClass I build Ethrex, one of the fastest Ethereum clients, a new programming language called Concrete designed around a formally verified kernel, and Lambdaworks, a cryptographic proof library used in production. I built the underwriting engine for Levenue, Europe's largest revenue-based financing platform. I'm helping develop a bank and a payments platform replacing broken financial rails in Latin America. Through Ergodic Group I hold companies across distributed systems, AI, gaming, wine, and culture. This site is where I write about what compounds over time rather than what trends today.
Talk
Blockspace Forum Cannes - Fede and Justin Drake
Discussion with Justin Drake at Blockspace Forum Cannes
Start here
- Notes on permanence, time, and ergodicity (the philosophical foundation behind everything else)
- The missing institution of the Internet (why Ethereum matters as infrastructure, not speculation)
- Transforming the Future with ZKPs (the cryptography that makes trustless systems possible)
- The Tail Hedge Debate: Spitznagel Is Right, AQR Is Answering the Wrong Question (the practical portfolio case for convexity)
- At the Core of Finance Lies Geometry. In the End, It’s All Jensen’s Inequality. (the mathematical capstone: compounding, Kelly, Jensen, and survival)
- The Death of the Inner Self (on consciousness, identity, and what technology dissolves)
- Friction as Luxury (why scarcity and difficulty create value)
- Fede's Guide to a Healthier Life (an ordered, evidence-based health guide for nerds)
Latest
Article
CommitLLM: How to Verify an LLM Inference
LLM APIs ask you to trust that the provider ran the model and settings they advertise. CommitLLM adds cryptographic receipts and audits without zero-knowledge prover costs.
Series · Concrete
What Concrete Makes Worse
Concrete's constraints have real costs. Linear cleanup is verbose, no closures hurt composition, and the ecosystem barely exists. Here is what the language actually makes harder.
Series · Concrete
When the Compiler Is the Oracle
I ran an autoresearch-style loop on a Concrete program. The compiler told an agent where authority, allocation, and proof surface could improve and confirmed when those properties changed. No profiler…
Series · Theorem Proving
Writing Your First Proofs in Lean
The same three theorems from the Python prover, now in Lean 4.
Series · Theorem Proving
Programming a Mini-Lean in Julia’s Type System
Guillermo Angeris builds a working theorem prover in 61 lines of Julia. A tiny trusted kernel, six axioms, and the compiler does the rest. This article walks through the full construction.
Series · Theorem Proving
Building a Tiny Theorem Prover in Python
A tiny theorem prover is just a term language, a checker, and a small trusted kernel. We build one in plain Python to make the architecture explicit.
Series · Theorem Proving
Propositions Are Types, Proofs Are Programs
The Curry-Howard correspondence says that types and logical propositions are the same thing. Understanding why changes how you think about both programming and mathematics.
Article
Self-Replicating Programs Emerge from Random Noise
Turing completeness is a shallow pit you fall into. Self-replication is an even shallower one. A recent paper shows that self-replicating programs spontaneously emerge from soups of random code, no de…
Article
Fede’s Guide to a Healthier Life
An ordered, evidence-based health guide for nerds who used to think the body didn't matter.
Series · Concrete
Can I prove Concrete programs in Lean?
I want to prove Concrete programs in Lean. The compiler already produces native Lean data as its IR, and the language is small enough that formalization might actually be tractable.
Series · Concrete
The AI Training Data Trap for Programming Languages Has an Exit
Edgar Luque is right that AI creates a new barrier for programming languages. He is wrong that the barrier is universal. Languages designed for machine generation and machine verification invert the p…
Series · Concrete
The Rust Effects Debate and Concrete’s Case for a Smaller Language
Wuyts is right about effects and ownership. The Hacker News skeptics are right about complexity. Concrete accepts both and says no to refinement types.
Series · Les Circuits Longs
Dissolution Without Construction
Every previous coordination technology that dissolved a form of selfhood also cultivated the next one. Current algorithmic systems only dissolve. The problem is the speed mismatch.
Series · Les Circuits Longs
Legibility Kills What It Measures
What happens when AI makes everything legible? The things that worked because they couldn't be seen clearly may stop working once they can.
Series · Leptokurtic
At the Core of Finance Lies Geometry. In the End, It’s All Jensen’s Inequality.
A 400-year journey through logarithms, Kelly, ergodicity, and tail risk to show why geometry sits at the core of finance and why Jensen's inequality ties the whole story together.
Series · Leptokurtic
The Tail Hedge Debate: Spitznagel Is Right, AQR Is Answering the Wrong Question
We tested Spitznagel's tail hedging strategy and AQR's critique with 17 years of real SPY options data. AQR's published tests use near-ATM puts in a no-leverage framing, two differences from the portf…
Series · Leptokurtic
Detecting Crashes with Fat-Tail Statistics
We built fatcrash, a Rust+Python toolkit with 15 crash detection methods: LPPLS, DFA, EVT, Hill, Kappa, Hurst, GSADF, momentum/reversal, price velocity, and more. Tested on 96 drawdowns across BTC, SP…
Series · Leptokurtic
Twenty Centuries of Financial Data: What 240 Countries and 2,000 Years Reveal
We assembled forex-centuries, an open dataset of exchange rates, gold, silver, interest rates, commodity prices, GDP, sovereign debt, and more — 27 sources spanning 1 CE to 2026, covering 240 countrie…
Series · Les Circuits Longs
Friction as Luxury: What We Lose When AI Gives Us What We Want
The scarcity that matters most in a post AGI world won't be compute or energy. It will be desire itself.
Article
China is trying to commoditize the complement
What happens to the West's services advantage when strong AI models are free, portable, and running on every laptop?
Article
Building a SaaS with Elixir/Phoenix and React
Our stack and practices for building SaaS applications: Elixir on the backend, React on the frontend, Nix for everything else. No Docker. No Kubernetes.
Series · Les Circuits Longs
Unprepared for What’s Coming
Humanity is completely unprepared for what's coming. The pace of AI advancement might give people months to adapt, not decades.
Article
Fede’s Guide to Type Systems: From Generics to Dependent Types
A practical guide through the landscape of type systems, from everyday generics to dependent types that prove correctness, with examples in Rust, Scala, and Idris
Series · Concrete
Why Concrete Exists
Concrete is a systems language designed so the compiler can reason about what code does: authority, allocation, resource lifetimes, and proof surface.
Series · Les Circuits Longs
The Death of the Inner Self
Individuality is a coordination technology. It emerged under specific historical conditions, and those conditions are weakening as computation, capital, and automated feedback loops absorb the functio…
Series · Les Circuits Longs
Notes on permanence, time, and ergodicity
Some businesses get better with time. Others lose their nerve, their standards, and their memory. This is about the difference.
Series · Ethereum
The new financial backend of the world
Ethereum is emerging as a neutral financial backend, lowering the cost of global financial services by encoding ownership and obligations in shared infrastructure.
Series · Ethereum
The missing institution of the Internet
The internet scaled information but not ownership institutions; Ethereum addresses this gap by embedding rights, records, and enforcement into programmable economic infrastructure.
Talk
Ethereum’s Native Rollup Roadmap with Justin Drake
Discussion about Ethereum's native rollup roadmap
Article
Crypto doctrine
Crypto found product-market fit where trust is weakest: inflationary or censored economies, and internet-native communities that need programmable coordination and markets.
Article
Zero-Knowledge Proofs and the Economics of Verification
The proving-verification asymmetry in zero-knowledge proofs is what makes them economically meaningful: proving is expensive, verification is cheap, and that gap changes what systems can be built with…