There is a wide range of software that exists in a "adversarial" environment, including anything facing a network or processing outside data. At a minimum, this software should should not allow an attacker to execute code of their choice on a system handling private data.

This does not require proving systems complete correct, but it does involve proving many properties of these systems.