Skip to Content


TLA+ is a blueprint language for software: you don’t build a house without plans, and you shouldn’t write complex software without planning it either. By writing a TLA+ specification, you can detect and remove complex bugs from your system before writing a single line of code.

TLA+ is especially useful for building distributed systems, cloud computing, and complex business domains: all things that regular testing is inadequate for. Amazon found formal specification so useful they started budgeting annual engineering time to writing them.

eSpark Learning, a product company with ten engineers, found that TLA+ cut development time by 25%. The systems were far more efficient and reliable: one system went from having one critical issue each week to zero in ten months.

TLA+ allowed us to deploy especially complex code critical to building new partnerships ahead of time with no substantive issues in production. - Blake Thomas, Director of Engineering, eSpark Learning

I am considered one of the foremost experts in teaching and applying TLA+. My tutorial Learn TLA+ receives over 2,000 visits each month and I am the author of the Apress book Practical TLA+.

I am now offering private workshops to interested companies. Over the course of three days, attendees will learn how to apply TLA+ to a wide variety of problems, including distributed systems, business workflows, and low-level code. Lessons can be tailored to the specific problem domain of the company. Contact me here to learn more.