“Foolish consistency,” Emerson claimed, “... is the hobgoblin of little minds.” We agree! The problem, in both philosophy and distributed computing, is to figure out when consistency is foolish and when it is absolutely necessary. Fortunately, formal methods technologies can help us address this problem. Galois and our partner Twisp have been using the P language for systematic concurrency testing to separate foolish from necessary consistency in production fintech applications. Double-entry accounting has remained unchanged for centuries. Twisp set out to modernize the age-old concept on a new distributed data storage system. Every financial system has some kind of distributed storage system underlying it—this is just as true for a cryptocurrency and a traditional bank. These ledger systems record the financial state of every account, and allows users to transact (for example, spend, save, or check their balance). When you use a credit card online, take money out of an ATM, order dinner on your couch or in Australia, you are interacting with a global-scale distributed storage system. Twisp’s core accounting engine is a correct, fast, and secure ledger platform suitable for fintech applications from small to large. It’s critical that a financial system is accurate and reliable, and so right from the start, Twisp integrated formal methods technologies into their design process. Familiar with our deep-rooted experience in provable security and model-based assurance, Twisp reached out to Galois in 2021 and asked us to help them build a system with world-class reliability and correctness. But let’s back up a moment. How does this all relate to consistency? And why is consistency so hard to get right? Consistency, in a distributed financial system, tells us who knows what, when. Imagine you’re in Istanbul and I’m in Tokyo. If you ta