A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss | Code BEAM V

TALK LEVEL: BEGINNER / INTERMEDIATE / ADVANCED

This talk introduces TLA+ by taking a small package from hex, examining its properties, modeling its behaviour as a state machine, creating TLA+ correctness and liveness specifications for it, and then using the TLA+ model checker to prove correctness. No prior exposure to formal methods like TLA+ or PlusCalc are necessary. A passing familiarity with state machines is recommended, but not required.

THIS TALK IN THREE WORDS

Formal

State

Machines

OBJECTIVES

  • Introduce TLA+ and its value
  • Illustrate conversion of a state machine to a TLA+ specification
  • Building and checking correctness and liveness models of that TLA+ specification

TARGET AUDIENCE

Developers interested in adding more rigour to their problem solving and more quickly surfacing design errors.

Upcoming conferences

Start booking your calendar with more Code Sync conferences happening across the globe. We will be slowly releasing more dates, in the meantime here is what we’ve planned already:

All conferences