For any sufficiently powerful system (Turing completeness is definitely powerful enough) there are statements which are true but cannot be proven by that system. Secondarily, no system can demonstrate its own consistency.
However, if you limit your software enough, you can prove that every possible input is handled correctly. That involves removing Turing completeness. E.g. once you accept a language as a configurator, you can no longer prove that. CSS3 is Turing complete. JSON is not.
One requirement is limiting the size of inputs.