Solving Riddles with Z3: An Intro to Formal Methods

**Let’s add the power of formal methods to our toolkit!**

*This is a joint session with Sacramento Software Engineers at Bloom Workspaces.*

We’ll explore Z3, a high-performance theorem prover from Microsoft Research. Z3 is widely used in formal verification, program analysis, and constraint solving.

We’ll learn the basics of Z3 by using the Python interface to solve a series of riddles from the TED-Ed YouTube channel.

*All coding will be done in Google Colaboratory – feel free to bring your laptop if you want to code along!*

**Who should attend:**
This session is for anyone curious about automated theorem proving and formal methods. Some familiarity with Python will be helpful, but no prior experience with Z3 or formal methods is expected.

**Agenda:**
6:30pm – Doors open.
7:00pm – Presentation starts.
8:00pm – Open discussion.
8:30pm – Meeting ends; we’ll head to a nearby restaurant or bar for more socializing.