Skip to Content

Consulting

Contact me here.

Services:

Workshops

If you’re building complex, expensive systems, my workshops on software modeling can help you save hundreds of thousands in saved developer time and maintenance work. With my training you’ll learn how to

  • Catch complex bugs that would take weeks or months to fix, and fix them before you start writing code.
  • Build complicated systems quickly and with confidence.
  • Better understand, document, and modify existing legacy systems.

My Training

I combine deep subject mastery with extensive teaching experience and cutting-edge learning innovations. I teach workshops so that students learn, not just check a box in the training budget. My training includes:

  • Lessons customized to the skill level of the attendees
  • A wide variety of hands-on labs, group exercises, and skill scaffolds
  • Guided mentoring on modeling production systems at your company
  • Post-workshop office hours and followup assessments

My prior clients include Netflix, Cigna, NASA, HCA, Ramp, and CrowdStrike.

Workshops are for one to three days, depending on the scope of training, and can be for up to 15 people at a time. I specifically offer workshops in TLA+ and Alloy. Workshops are also available remotely and can be adapted to a company’s schedule, such as by three half days instead of two full days. Email me here if you want to learn more.

Software Modeling Case Studies1

AWS
Amazon modeled DynamoDB and S3, finding complex bugs in both. One was so complicated that “the shortest error trace exhibiting the bug contained 35 high level steps”. They had slipped past all their tests, QA, and code review, and would have lost customer data if it reached production. They also confidently made several performance optimizations and were able to test they didn’t lead to problems later. One engineer later estimated that software modeling cut two months off a four-month schedule.
eSpark Learning •
The infrastructure team at eSpark Learning was just two engineers. They needed to refactor a large system to handle the extra load from a high-value customer, with the requirement that the system should have no issues in production. Two days of modeling caught several major bugs in the new version, bugs that would have lost the customer’s business. This saved 200k/year in revenue and an additional 100k/year in saved developer maintenance.

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

Rackspace
By modeling an existing production system, Rackspace found a bug so severe they needed to redo a year of work. If they had started using models from the start, they would have saved a year of work for the entire team.
OpenComRTOS
OpenComRTOS is a real-time operating system (RTOS) written start-to-finish entirely with debuggable designs. OpenComRTOS is 10x smaller than comparable embedded OSes, which the developers directly attribute the time they spent modeling. The modeling also made it possible for junior developers to contribute to the complex system, as they could more confidently make and test changes.

Cockroach Labs •
Cockroach labs modeled one of their critical performance optimizations. Their model found a complex bug that would have taken over ten hours to debug. More importantly, it gave them confidence that their fix actually worked, saving a lot of time on review and later testing.

Talks

I am available for paid corporate talks. My specialties are formal methods and the process of software engineering. I currently offer the following talks:

Designing Distributed Systems with TLA+

Sample is here. Duration is 30-40 minutes.

Distributed systems are hard. Even a few interacting agents can lead to tens of thousands or even millions of unique system states. At that scale, it’s impossible to test for, or even reason about, every possible edge case. We need better tools not just for building systems, but for understanding them. This talk will focus on one software modeling tool called TLA+, which has seen spectacular success in real-world businesses.

What We Know We Don’t Know

Sample is here. Duration is 30-40 minutes.

There are many things in software we believe are true but very little we know. This talk is all about how we empirically find the facts in software and some of the challenges we face, with a particular focus on software defects and productivity.

Are we really engineers?

Under Development. First draft of talk is available here. Duration is 30-40 minutes.

What makes software engineering different from “traditional” engineering? To find out, I interviewed 17 “crossovers”: people who have worked professionally as both a software and a traditional engineer. In aggregate, we learn three things: we are in fact engineers, we’re not actually that different as a field, and there’s a lot we can both teach and learn.

My book.
  1. Studies marked with a • are ones I worked with in an official capacity. [return]