LGTM Is Not A Theorem

My time at IBM, MathWorks, and AWS prior to my PhD taught me that software engineering principles are adaptable guidelines, not rigid laws. MathWorks demanded an exceptionally high bar for rigorous testing because its software simulates safety-critical systems. Conversely, AWS prioritized a first-mover advantage, driving rapid delivery. Ultimately, an organization’s testing bandwidth depends on whether the business goal is immaculate quality or speed-to- market. Navigating these philosophies means as an engineer you need to align yourself with a company’s operational reality and adapting to the business demand.

Is formal verification overrated? No. However, it is economically unfeasible if treated as an all-or-nothing pursuit of total correctness. This talk argues for a pragmatic middle ground: proving what we can, where it matters most. Moving up the assurance ladder shouldn’t require verifying an entire software stack. In a typical production setup, like a Django web server talking to a database, verifying the Python-to-JSON translation or the FFI is largely intractable. Instead, the buck stops at the interface. I show how to use formal methods to ensure core application contracts strictly abide by the expected specification, bypassing the messy infrastructure. We aren’t proving the universe; we just want to verify the critical layers in between.

The audience will walk away with a clear design mindset. This pivots the software engineering discussion away from endless code generation and toward the economics of formal properties. Instead of chasing the expensive illusion of total correctness, attendees will learn to target resources effectively at critical interface layers. Ultimately, this approach forces us to evaluate a vital question: does our target theorem represent a strong, structural property, or just a weak, superficial one?