[ChrisLomont]

Logic proving systems need never hit Godel incompleteness. Many systems weaker than Godel are proven consistent within themselves, and are strong enough to verify code.

Godel’s Proofs rely on statement encoding using properties of integers not required for these logic systems.

Presburger Arithmetic, for example, avoids Godel incompleteness, yet provides a decent system for a lot of work.