The topic for tonight is my favorite, Formal Verification. This security area aims to prove qualities about programs through math and logic. Some of those qualities include things like, a program has no buffer overflows, and prove that, none exist.