Article
A Proof Is Only as Good as Its Spec
Formal verification doesn't eliminate risk. It relocates it into the spec, the model, and the trusted base. Five runnable Lean 4 proofs that compile cleanly and still sit on real bugs.
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.
Series · Concrete
Nutrition Labels for Trust
Vitalik Buterin wants software to carry a nutrition label of its trust dependencies, and binji wants agents that read it for us. Concrete already builds the machine-and-math half of that label as a compiler artifact rather than prose: capabilities, proof obligations, evidence classes, axioms, and trusted boundaries.
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
Discipline Without Love Optimizes for the Wrong Variable
On pain, building, capitalism, discipline, and realizing I had treated love as something that came after the work.
Series · Concrete
A Fact-Producing Compiler
Concrete already knows a lot about what a program relies on: authority, allocation, recursion, trust, safety obligations, and proof evidence. The next step is making those facts easy for agents, CI, a…
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, hidden-capture closures are gone, and the ecosystem is still early. Here is what the language actually makes harder.
Series · Theorem Proving
Writing Your First Proofs in Lean
The same three theorems from the Python prover, now in Lean 4.
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
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. Here is the 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?
The original roadmap for proving Concrete programs in Lean, updated now that part of that bridge exists: source contracts, proof obligations, Lean-checked evidence, stale detection, and an explicit tr…
Series · Concrete
Designing a Programming Language for the AI Era
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
Finance Is Geometry, and It All Comes Back to Jensen’s Inequality
Logarithms, Kelly, ergodicity, and tail risk meet at the same geometry: wealth compounds multiplicatively, the logarithm is concave, and Jensen's inequality measures the cost of variability.
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. In the allocation-reducing framing AQR uses, selling SPY to fund puts, deep OTM puts lose at eve…
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, across 27 sources spanning 1 CE to 2026 and covering 240…
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.
Article
Fede’s Guide to Type Systems: From Generics to Dependent Types
A practical guide to 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.
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.
Series · When Rules Repeat: The Fixed Point Ladder
Markets as Reflexive Fixed Points
Markets are more than noisy aggregators of information: beliefs about prices help determine prices, which makes reflexivity a fixed-point problem with fat tails, non-ergodicity, and hysteresis.
Series · When Rules Repeat: The Fixed Point Ladder
Life as a Double Fixed Point
Living systems are not fixed points in the naive sense but robust attractors and self-reproducing machines, whose encoded description takes part in their own continuation.
Series · When Rules Repeat: The Fixed Point Ladder
Logic, Self-Reference, and Category Theory
Once arithmetic can encode syntax, a system can act on descriptions of itself. That second engine produces Gödel sentences, quines, the Y combinator, recursive types, and Lawvere's fixed point theorem…
Series · When Rules Repeat: The Fixed Point Ladder
Number Theory and the Arithmetic of Recurrence
Once a rule repeats in time, integers appear. Recurrence, resonance, continued fractions, and KAM theory show how arithmetic decides which motions are stable and which fall apart.
Series · When Rules Repeat: The Fixed Point Ladder
Power Laws, Extremistan, and Non-Ergodicity
Scale invariance becomes power laws; power laws move importance to extremes; extremes make averages unstable through time.
Series · When Rules Repeat: The Fixed Point Ladder
Chaos, Fractals, and Renormalization
How period-doubling creates chaos, why Feigenbaum universality appears, and how fractals become fixed points of set-valued contraction maps.
Series · When Rules Repeat: The Fixed Point Ladder
Fixed Points and Attractors
The foundation of the ladder: repeated rules, dynamical systems, fixed points, attractors, basins, bifurcations, Newton iteration, and the logistic map.
Series · The Edge of Chaos
When Risk Models Create Risk
The last essay said the tail is too hard to measure. Jón Daníelsson goes one step further: in finance, the measurement itself changes the thing measured. When everyone uses the same risk model, the mo…
Series · The Edge of Chaos
The Limits of Knowing
Every method in this series rests on one number: how close a system sits to its edge. Nassim Taleb spent a career arguing that this is exactly the number you cannot trust. For fat-tailed systems the d…
Series · The Edge of Chaos
Why the Calm Is Dangerous
A system heading for a tipping point gives off warning signs in unexpected places. The danger rarely arrives as drama and rising volatility. It hides in the calm. Ecologists learned to read it in lake…
Series · The Edge of Chaos
What Actually Moves Prices
The series has argued that markets move themselves, but there is now a clean mainstream number for that claim. Gabaix and Koijen estimate that one dollar flowing into the stock market raises aggregate…
Series · The Edge of Chaos
Reflexivity by the Numbers
Everyone agrees markets react to themselves. The question is how much. A statistical tool built for earthquakes turns that vague idea into a single number: the fraction of market activity that is the …
Series · The Edge of Chaos
Faster Than Exponential: Can You See a Crash Coming?
The last essay said big cascades are built in and the trigger tells you nothing. Didier Sornette disagrees, at least about the biggest ones. He argues a bubble grows faster than exponentially toward a…
Series · The Edge of Chaos
Sandpiles and Crashes: How Systems Tune Themselves to the Brink
The last essay left a loose end. Markets can sit near a critical edge where small shocks cascade, but critical points are usually finely tuned, so who keeps a market balanced there? The answer, found …
Series · The Edge of Chaos
Crashes Without a Cause: Markets as Phase Transitions
Big market moves often show up with no news to explain them. A hundred-year-old model of magnets shows why. When people copy each other strongly enough, a market can hold two moods at once, and the sm…
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…