This is how I see a way to formalize your question. Long addition operates on strings of decimal digits. On the other hand, we can define our basic addition, which is our starting point, to operate on strings of 1's (unary notation), or, equivalently, on terms of the form S(S(...S(0)...)) (here S stands for "successor"). We can define unary addition and multiplication by recursion as follows.
0 + y = y
S(x) + y = S(x + y)
x * 0 = 0
x * S(y) = x * y + x
These definition are supposed to express our intuitive concept of addition and multiplication and act as a starting point.
We can also define a translation from decimal to unary strings, also by recursion:
f(0) = 0
f(1) = S(0)
f(2) = S(S(0))
f(9) = S(S(S(S(S(S(S(S(S(0)))))))))
f(ds) = S(S(S(S(S(S(S(S(S(S(0)))))))))) * f(d) + f(s) where d is a decimal digit and s is a string of decimal digits.
Finally, we define long addition on decimal string. Let's denote it by add(s1, s2). Then correctness of long addition (with respect to unary addition) means that
f(s1) + f(s2) = f(add(s1, s2)) for all decimal strings s1, s2.
Similar theorems for binary addition were formally proved using proof assistants like PVS, Coq and Isabelle.