Presented by

  • Jon Manning

    Jon Manning

    Jon Manning is the cofounder of independent game development studio Secret Lab. He's working on the critically acclaimed award-winning adventure game Night in the Woods, which includes his interactive dialogue system Yarn Spinner. He's written a whole bunch of books for O'Reilly about iOS development and game development. Jon holds a PhD about jerks on the internet.


Automated theorem provers allow you to describe a set of logical assertions and constraints, and then discover inconsistencies and impossibilities in that system. This makes them incredibly useful for testing large, complicated and intricately interlocking systems. Sounds like a video game. In this talk, we’ll use Z3, an open source theorem prover from Microsoft Research, to describe and diagnose problems in an RPG, and automatically discover problems like softlocks and impossible situations. We’ll unpick some of the impressively dense jargon that often surrounds this field, and learn how to apply this theory to practical effect. By the end of this talk, you’ll be ready to apply formal logic to game systems, how to create an abstract model of a complex game, and how to find and fix bugs that you didn’t know you had. You'll also be ready to apply these learnings to non-game systems, too!