Federico Ponzi

I've contributed a TLA+ formatter to the official tlatools. It is also integrated into the VS Code extension. In this article I want to share a few thoughts on what I've learnt along the way about what it takes to write a formatter: blog.fponzi.me/2026-03-30-a-p…

Reading the AWS postmortem, and the HN reaction to it, and: I will never stop evangelizing this, the most brain-altering piece of writing I've encountered. howcomplexsystems.fail

Kyle Kingsbury Jepsen’ed TigerBeetle jepsen.io/analyses/tiger…

Very proud to announce that the Windows Subsystem for Linux is now open source! blogs.windows.com/windowsdevelop…

🔧 GenAI-Accelerated #TLAplus Challenge is live! Use GenAI to enhance TLA⁺ specs, tools, or workflows. Submit your project for a chance to win a prize. Details: foundation.tlapl.us/challenge/inde…

i’m a big fan of Domain Driven Development first i buy the domain and eventually i develop the app

An excellent primer (and then some) on "target triples," a concept that most systems-level programmers must have a good grasp of eventually. I fumbled my way through understanding this over the past many years but this resource is a great starting point: mcyoung.xyz/2025/04/14/tar…

HELP PRESERVE OUR LIMITED SUPPLY OF UUIDS! instead of generating a new UUID, try to reuse one you already have!

Thrilled to announce... devblogs.microsoft.com/typescript/typ…

i saw a clueless someone post this image as an attempted dunk on NASA in favor of SpaceX this is actually the correct approach. (see why in thread)

@Jeevananthan05 @DistribSystems Because you mentioned her talks, I was curious to know if there are other talks by her you would recommend?

@federico_ponzi @DistribSystems In what genre?

Let's Talk Locks! Kavya Joshi explores when and why locks affect performance, delves into Go’s lock implementation as a case study, and discusses strategies one can use when locks are actually a problem. buff.ly/41mCpQ7

@Jeevananthan05 @DistribSystems Do you have other talks to recommend?

@DistribSystems Her talks made me understand even more how to understand the Theory of Computation.

TIL about Q# programming language for quantum computers, it's also open source: learn.microsoft.com/en-us/azure/qu…

How Libra Was Killed. I never shared this publicly before, but since @pmarca opened the floodgates on @joerogan’s pod, it feels appropriate to shed more light on this. As a reminder, Libra (then Diem) was an advanced, high-performance, payments-centric blockchain paired with a stablecoin that we built with my team at @Meta. It would’ve solved global payments at scale. Prior to announcing the project, we spent months briefing key regulators in DC and abroad. We then announced the project in June 2019 alongside 28 companies. Two weeks later, I was called to testify in front of both the Senate Banking Committee and the House Financial Services Committee, which was the starting point of two years of nonstop work and changes to appease lawmakers and regulators. By spring of 2021 (yes they slow played us at every step), we had addressed every last possible regulatory concern across financial crime, money laundering, consumer protection, reserve management, buffers, and so much more, and we were ready to launch. We had worked on a slow rollout of a limited pilot that some members of the Fed’s Board of Governors were supportive of. At last, Chair Jay Powell was ready to let us move forward in a limited way. The story, as I heard it, is that Jay Powell was told by Treasury Secretary Janet Yellen at one of their biweekly meetings that allowing this project to move forward was “political suicide,” and she would not have his back if he let it happen. I wasn’t in the room when this conversation happened, so take these words with a grain of salt, but effectively this was the moment Libra was killed. Shortly thereafter, the Fed organized calls with all the participating banks, and the Fed’s general counsel read a prepared statement to each of them, saying: “We can’t stop you from moving forward and launching, but we are not comfortable with you doing so.” And just like that, it was over. One essential point is worth making here. There was no legal or regulatory angle left for the government or regulators to kill the project. It was 100% a political kill—one that was executed through intimidation of captive banking institutions. That was the hardest part of this story for me personally. Not that we had failed, but that America, this country I immigrated to and became a proud citizen of because of its rule of law and value system, behaved in such a way for political reasons. It was a very tough pill to swallow. The bright side of the story, though, was the many learnings from this wild ride. By the end of the project, we had made so many concessions to get a thumbs-up that the whole design of the network became a Frankenstein of our initial ambitions. We also learned the biggest lesson of all, which is that if you’re trying to build an open money grid for the world—eventually moving trillions of dollars a day, designed to be here 100 years from now—you have to build it on the most neutral, decentralized, unassailable network and asset, which, hands down, is Bitcoin. And now this is what many of us who went through this scarring journey are building together at @Lightspark. And this time, we won’t stop until we get it done!

Save the date! The TLA+ Community Event 2025 will take place on May 4, 2025, in Hamilton, Canada. This marks a first for our academic conference, as it will be held outside Europe for the very first time. conf.tlapl.us/2025-etaps/ #tlaplus

We are Akka! We’re excited to announce that Lightbend is now Akka. Our name change better reflects who we are as a company and the mission we stand for. Even bigger news is Akka 3 - a platform to build and run apps that are elastic, agile, & resilient. bit.ly/3Z68z17

Do you like computers? Check out my 8-bit breadboard computer: blog.fponzi.me/2024-10-15-my-…

Me: Can your Vim do that?! Vimmers: Yes! Just do jlsdfgjlsh7*&#H12828H@3@(*((...

@muratdemirbas What a milestone! Congrats Murat 👏 looking forward to the next 700 😊

[new blog post] 700 muratbuffalo.blogspot.com/2024/10/700.ht…

@mehfdfsda @DistribSystems More resources: learntla.com and if you get stuck or have questions, reach out to the community: federicoponzi.github.io/tlaplus-wiki/c…

@mehfdfsda @DistribSystems You can get started quickly by using the tlaplus-vscode plugin: github.com/tlaplus/vscode… after you get a basic understanding of tla+, I would recommend learning pluscal (which is translate to TLA+) it's a bit easier to write. Lamport's book is also very easy to follow.

Validating Traces of Distributed Programs Against TLA+ Specifications: arxiv.org/pdf/2404.16075 A framework for relating traces of distributed programs to high-level specifications written in TLA+.