As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of techniques to ensure that.

1. compiler-like timestamp mechanism: GNATprove uses the timestamps of the generated ALI and Why3 files to know whether some source file is more recent than the local effects (in ALI files) and Why3 code (in Why3 files) that was generated from a previous version of the same file. As a result, if a source file and all the files on which it depends have not been modified, the corresponding Why3 intermediate file is not regenerated, and no new proof is even attempted.
2. VC hashing mechanism: For every VC that is proved, GNATprove stores a MD5 hash of the proved VC file. Before any attempt at proving a new VC, its MD5 is compared to that of proved VCs, so that proof is only attempted for yet unproved VCs.
3. VCs based on semantic dependencies: Generation of VCs only depends on the semantic closure of dependencies between entities, not on dependencies between files. So even if some file has changed, many VCs in this file and other files that depend on it will not be changed, and by point 2 above, no proof is attempted if the VCs were proved previously.
4. persistent storage of proof results: GNATprove stores all proof results in a session file, which can be shared between developers in Configuration Management. A typical workflow would be to run GNATprove nightly on a server, and update the shared session file from that run. All developers can retrieve an up-to-date session file before running GNATprove locally, thus benefiting from all proofs done in the nightly run.

Something that is not implemented in GNATprove yet is the capability to share proofs that are not stored in the current session file, either because they correspond to previous proofs now obsolete, proofs performed on other branches of the source code, or proofs done concurrently by another developer on his machine. A mechanism for centralized hashing of proved VCs (like was done in SPARK 2005 using memcached) would provide this additional level of proof sharing.See SPARK User's Guide for more tips on how to use GNATprove in a team.

For another proof environment implementing similar techniques, see section "On-demand Re-verification" in the article "The Dafny Integrated Development Environment" by Leino and Wüstholz.