While formal verification has been applied with great success in several projects, automating verification techniques to a degree that they can be incorporated in day-to-day software development remains a somewhat distant dream. It is however possible to use formal methods, such as those employed in verification, in environments with large programs and frantic development speeds! Not to prove theorems that such programs have *no* bugs (they do!), but instead to automatically prove that such programs *do* have bugs. In this talk I’ll share some insights gained while turning program verification techniques into bug-finding tools to help programmers at scale.