Recently, I had the opportunity to lead the development of a real estate fintech platform.

The platform wasn’t just about transferring money between accounts. Users could also purchase entire properties or buy fractional ownership in properties.

This made things considerably more interesting from an engineering perspective.

We were dealing with properties worth hundreds of millions of naira, with transactions that could easily exceed ₦1 million.

When you’re building something that handles money at this scale, mistakes can be extremely expensive. A single overlooked edge case could potentially cost the business or its customers millions.

One thing I constantly had at the back of my mind while designing the system was how do I find the edge cases I haven’t thought of?

Of course, you can write tests, review your architecture, think about concurrency, implement database transactions, and follow established engineering practices.

But what about the scenarios you don’t even know exist?

This was particularly important to me because it was my first time leading a fintech project. I didn’t have years of experience dealing with financial systems or the countless edge cases that experienced fintech engineers might have encountered.

I needed something that could help me challenge my assumptions about the system before it went into production.

That’s how I came across TLA+.

What exactly is TLA+?

TLA+ is a formal specification language developed by Leslie Lamport. It’s used to describe and reason about how systems behave using mathematics.

That might sound complicated, but the idea behind it is relatively simple.

Let’s say you’re designing a system with multiple components interacting with each other.

You already have an idea of how everything should work. You know the operations that should be allowed, how the system should transition between states, and what should never happen.

TLA+ allows you to describe these rules mathematically.

You can then use a model checker, such as TLC, to systematically explore the possible states and sequences of operations in your model.

If the model allows something that violates one of your rules, TLC can show you a sequence of events that leads to that violation.

In other words, instead of relying entirely on your ability to imagine every possible failure scenario, you can let a tool explore scenarios you might have overlooked.

However, this exploration is only as comprehensive as the model you’ve written and the scope you’ve configured.

A simple fintech example

Let’s use fractional property ownership.

Imagine a property has been divided into 100 shares, and only one share is left.

Two users, Alice and Bob, attempt to purchase that last share simultaneously.

Here’s one possible sequence of events:

  1. Alice checks the number of available shares. The system returns 1.
  2. Bob checks the number of available shares. The system also returns 1.
  3. Alice proceeds with her purchase.
  4. Bob proceeds with his purchase.
  5. Both transactions succeed, even though only one share was available.

You’ve now allocated two shares when only one existed.

Race condition in fractional property ownership

An experienced developer would probably recognize this as a concurrency problem and consider database locking, atomic updates, or other concurrency controls.

But concurrency isn’t always this straightforward.

Consider another scenario.

A user attempts to purchase a property. The payment is successfully processed, but the API response times out before the client receives confirmation.

The client retries the request.

What happens next?

Does the system recognize that the original transaction succeeded? Does it charge the user again? What if the payment succeeded but the ownership record wasn’t created?

These are all questions your architecture needs to answer.

And even if you’ve designed a solution for them, you still need to consider whether unexpected sequences of events could break that solution.

This is where TLA+ becomes useful.

You can model the different states of a transaction, the operations that change those states, and the rules that must always hold.

For example:

  • A property must never have more ownership shares allocated than exist.
  • The same purchase request must not result in duplicate charges.
  • A failed transaction must not silently result in an inconsistent financial state.
  • A successfully processed purchase must have a defined path to ownership allocation or recovery.

You then check whether your modeled system can violate these properties.

If TLC finds a violation, it provides a counterexample showing how the system reached that state.

TLC model checker exploring system states and detecting invariant violations

For me, this was one of the most interesting things about TLA+.

It’s not just about finding obvious bugs. It’s about discovering unexpected interactions between operations that individually appear perfectly reasonable.

My first mistake using TLA+

One thing I learned relatively quickly was that you shouldn’t try to model your entire application at once.

When I first started experimenting with TLA+, I made the mistake of giving my AI coding agent too much scope.

Instead of focusing on one critical operation, I tried to verify too much of the system together.

The result was a model that took much longer to check than I expected.

There’s a reason for this.

Model checking can suffer from something called state-space explosion.

As you introduce more variables, operations, users, and possible states, the number of combinations the model checker needs to consider can grow extremely quickly.

A relatively small model might finish in seconds, while a much larger one could take hours or exhaust the available memory.

State-space explosion in full app model vs fast verification in scoped model

My recommendation is to start small.

Identify the critical parts of your system where mistakes would have the greatest impact.

For a fintech application, I’d probably start with money transfers, transaction state transitions, idempotency, and ownership allocation.

Model those behaviors individually where possible, while keeping together any interactions needed to verify a particular rule.

Then gradually expand the model when necessary.

You don’t need to model every endpoint or database table. What matters is capturing the essential behavior and assumptions of the operation you’re trying to verify.

What TLA+ won’t do for you

I think this is important to understand before adopting it.

TLA+ is not a magical tool that guarantees your application is correct.

It helps you reason about the correctness of a system specification.

That doesn’t automatically mean your implementation is correct.

You could write a perfectly valid TLA+ specification, verify its properties, and still implement the actual application incorrectly.

For example, your specification might assume that a database operation is atomic.

But if your implementation performs that operation through multiple independent database queries without the necessary transaction guarantees, the assumptions in your model no longer match reality.

TLA+ also cannot discover scenarios you completely excluded from your specification.

If your design assumes a dependency is always available, the model checker won’t spontaneously introduce database disconnections unless you’ve modeled that possibility.

And even when a model passes verification, the result applies to the properties, assumptions, and model configurations you checked.

It isn’t a universal proof that your production system can never fail.

You still need unit tests, integration tests, concurrency testing, fault injection, code reviews, and proper database safeguards.

I see TLA+ as something that complements these practices rather than replaces them.

Some disadvantages worth knowing

Beyond the potentially expensive model-checking process, there are other challenges.

  • The learning curve: TLA+ uses mathematical concepts and notation that can feel unfamiliar, especially if you’re used to expressing everything in code.
  • Modeling takes effort: Writing a useful specification requires you to understand your system well enough to describe its essential behavior precisely.
  • Incorrect assumptions: A model can pass verification even when it doesn’t accurately represent how the real application behaves.
  • Limited practical coverage: Model checking a finite configuration doesn’t automatically establish correctness for every possible system size or operating condition.

These limitations don’t make TLA+ less useful. They simply mean you need to understand what you’re verifying and what conclusions you can reasonably draw from the results.

Is TLA+ actually used in production engineering?

Yes, and this was one of the things that made me interested in exploring it.

One of the resources that caught my attention was Amazon’s paper, How Amazon Web Services Uses Formal Methods.

AWS engineers have used TLA+ to reason about critical distributed systems, including work related to DynamoDB, S3, and other infrastructure services.

What’s particularly interesting is that they found subtle design errors that had survived traditional engineering approaches such as testing and code reviews.

Microsoft has also used TLA+ in Azure, including work on Cosmos DB’s distributed algorithms.

MongoDB engineers have applied it to replication, distributed transactions, and other complex protocols.

So this isn’t just an academic technique. Engineers have used it to solve real problems in large production systems.

Other tools worth exploring

TLA+ isn’t the only tool in the formal methods and correctness space.

PlusCal is worth exploring if you prefer writing algorithms in a style closer to pseudocode. It translates into TLA+, allowing you to use the same model-checking tools.

Apalache is an alternative model checker for TLA+ that uses symbolic techniques rather than explicitly enumerating states like TLC.

Alloy is another formal modeling language that allows you to describe constraints, explore possible structures, and find counterexamples.

Jepsen is also worth looking into, particularly for distributed systems. Unlike TLA+, which primarily works with abstract specifications, Jepsen tests running systems and introduces faults to look for consistency violations.

They serve different purposes, but they’re all interesting tools for engineers who care about system correctness.

What I’m currently working on: Regel

One of the biggest friction points with TLA+ is that it requires learning an entirely separate mathematical language. For most engineering teams, the syntax overhead prevents them from ever adopting it into their regular workflow.

Because I wanted the verification rigor of TLC without having to step outside of Go, I’ve been building Regel (German for “rule”).

Regel lets you write TLA+ models in readable Go. It compiles your specifications into real .tla and .cfg files, executes the real TLC model checker, and returns the verification results and counterexample traces directly as Go data:

spec := regel.New("Withdraw").
	Var("balance", 100).
	Workers("a", "b").
	Step("check", regel.If("balance >= 60").Goto("debit").Else("done")).
	Step("debit", regel.Set("balance", "balance - 60")).
	Always("NoOverdraft", "balance >= 0")

If a race condition or invariant violation exists, TLC flags the exact step-by-step trace that breaks it—before writing production code or waiting for a rare bug to surface in production.

It’s currently an active work in progress. If you find the project interesting or want to support it, check out the repository on GitHub and give it a star ⭐: github.com/sodiqscript111/Regel. Feedback, ideas, and contributions are always welcome!

Final thoughts

My biggest takeaway from experimenting with TLA+ is that writing code correctly and designing a correct system are two different problems.

You can have excellent code that faithfully implements a flawed design.

And sometimes the most dangerous problems aren’t caused by an obvious programming mistake. They’re caused by a particular sequence of events that nobody considered during development.

That’s the problem TLA+ helps address.

I don’t think every application needs formal verification, and I certainly wouldn’t recommend modeling every feature you build.

But if you’re working on financial systems, distributed infrastructure, or anything where certain failures could have serious consequences, I think it’s worth exploring.

Even if you never become an expert in TLA+, the process of explicitly defining what your system must guarantee can improve how you approach system design.

And if a model checker helps you discover a critical design mistake before it reaches production, the effort might already have paid for itself.

References and further reading