Skip to Content


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

Formal Specifications are blueprints for software: you don’t build a house without plans, and you shouldn’t write complex software without planning it either. By writing a specification, you can detect and remove even the most complex bugs from your system before writing a single line of code. Formal specification is especially useful for building distributed systems, cloud computing, and complex business domains: all things that regular testing is inadequate for. Amazon used formal specifications to design parts of S3 and DynamoDB and found it so useful they started budgeting annual engineering time to writing them.

But you don’t have to be as big as Amazon to benefit. At eSpark, we were a small (10 engineers total) product company that curated iPad apps for schools. By our estimates, using formal methods 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. You can read about our first success story here.


I will work with you to write a spec of a new or existing system. You will be able to automatically verify whether or not it does what you expect. By checking and refining the spec, you’ll be able to ensure that fundamental design issues are caught before they become problems.
Training and Workshops
I will provide training on how to use formal specification, with lessons adapted to your particular problem domain. You’ll learn how formal specification can help you specifically and how to begin applying it.

About Me

I am an expert in both teaching and applying formal methods with a specialization in Alloy and TLA+. I am the author of Learn TLA+, widely considered one of the best introductions to formal methods, and currently writing Practical TLA+ (Apress, est. September 2018). I’ve spoken multiple times on all forms of formal methods, most notably at Strangeloop 2017 and the Future of Alloy Workshop 2018. I am on the Alloy adoption and outreach working group.


Email me here.