Let’s Use An Automated Theorem Prover To Verify Video Games; I Swear This Is More Fun Than It Sounds
summary
Uses the Z3 SMT solver via its Python API to encode RPG decision variables (booleans and integers), check satisfiability of intertwined win conditions, and produce concrete models of required player choices or prove impossibility. Demonstrates finding Mass Effect 3 constraints that either allow or forbid the quarian/geth peace, extracting an unsat core to pinpoint conflicting rules, and using the optimizer to maximize or minimize companion approval in Dragon Age. Also finds unreachable voice lines and other scripting holes.
AI-written summary · about
chapters (7)
- 0:00Start
- 6:08HOW TO SAVE TWO SENTIENT SPECIES IN 6 EASY STEPS
- 6:54THE ACTUAL MATH, PART 2
- 8:49PROPOSITIONAL LOGIC
- 9:14LOGICAL OPERATORS
- 25:27APPROVAL RATINGS ARE INTEGERS
- 32:16FURTHER READING
related talks
20mNegative/Positive Verification for WorldGuard, CHERI and Other RISC-V Security Models-
23mBeyond Tests What to Verify in AI Generated Code
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
01h 02mPlaying Video Games One Frame at a Time
59mTest Driving Code with the Help of AI
48mA board game night with geeks
43m(Programs), Proofs and Refutations (and Tests and Mutants)
21mValidating SMT Solvers for Correctness and Performance via Grammar-based Enumeration