This talk will present results from a number of SPARK projects, concentrating on
theorem proving completeness for common program properties, such as freedom from
buffer overflow and other run-time errors. The results show a useful improvement
in completeness, but also highlight the limits of heuristic-based theorem proving.
These deficiencies suggest areas for future work, including constraint solving and
SAT-solving, that might improve the usefulness of such verification environments.
