Loop invariant for adding 2 arrays storing binary value of integer
Step 1: Fix the typo in c[i=]. That's obviously wrong. (Done). 

Step 1a: Try what happens when your algorithm adds 11 and 01. Notice that the result is wrong. 

Step 1b: Fix the bug in your code. Check what happens in your algorithm again. 

Step 2: Write down what is true at the end of the function which proves that the code is correct. 

Step 3: Write down what is correct after the last iteration where i = 1, before setting C [1] = carry, which will lead to the statement in Step 2. 

Step 4: Write down what is correct after each loop iteration, for each value of i. 

Step 5: Write down what must be true before each loop iteration to get the result in Step 4. 

Step 6: Figure out how Step 4 leads to Step 5. 

Step 7: Check that Step 5 is true before the first iteration.