[smallnamespace]

Note that Godel's Incompleteness Theorems tell us that formal systems with sufficient power cannot 'prove themselves' in some sense, and we see that rather convincingly:

1. Implementations can be wrong, so we want a formal proof system

2. The proof system can be wrong, so we want to apply the proof system to itself

3. But the proof system may be wrong (either in implementation or specification) in a way such that its self-proof is actually invalid

At some point, we want to assert some property (completeness, correctness) of the system as a whole, but whenever we augment the system to allow this, that augmented system's own properties now come into question.

[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.