Both static and dynamic program verification approaches have significant disadvantages when considered in isolation. Inspired by research on gradual typing, we propose gradual verification to seamlessly and flexibly combine ...