Carry computation with sympy (https://codegolf.stackexchange.com/a/140655/72753)

blind-binary-adder-proof.py

from sympy import *
from sympy.abc import i

zs = [0]*16
aux = [0]*16
bux = [0]*16
cux = [0]*16
dux = [0]*16

# step 1 : z0, aux, bux
for i in range(16):
    aux[i] = Indexed('a',i) + Indexed('b',i)
    bux[i] = Indexed('a',i) * Indexed('b',i)
zs[0] = bux[0]

# step 2: z1, cux, dux (cux can be computed at previous step)
for i in range(1,16):
    cux[i] = aux[i]*aux[i-1]
    dux[i] = aux[i]*bux[i-1]

zs[1] = aux[1]*zs[0] + bux[1]

# next steps
for i in range(2,15,2):
    zs[i] = aux[i]*zs[i-1] + bux[i]
    zs[i+1] = cux[i+1]*zs[i-1] + dux[i+1] + bux[i+1]

# check values
cs = [0]*16
cs[0] = Indexed('a',0)*Indexed('b',0)
for i in range(1,16):
    cs[i] = Indexed('a',i)*Indexed('b',i)+Indexed('a',i)*cs[i-1]+Indexed('b',i)*cs[i-1]

for i, (c,z) in enumerate(zip(cs, zs)):
    print ("check"+str(i))
    assert expand(c-z) == 0, "{0} => {1}".format(i, expand(c-z))