Verifying encrypted addition Alice has two secret numbers, a and b. She publishes c1=E(a), c2=E(b) and c3=E(a+b). Is there an encryption system E such that anyone would be able to prove that the c3 as published by Alice is actually E(a+b)?

EDIT: Modified the question to use "anyone" instead of "Bob".

Note that this is different from homomorphic encryption. In case of homomorphic encryption Bob is able to compute E(a+b) himself, but he is not necessarily able to prove that E(a+b) as computed by Alice is correct. What's needed here is a system where Bob is not necessarily able to compute E(a+b) but is able to prove Alice's result.
One example of such a system is ElGamal over a group $G$ generated by $g$. The public key is $y$ and an encryption $(x,w)$ of a message $m$ is of the form $(g^r, y^r m)$ for some integer $r$.

You have three ciphertexts $(x_1, w_1)$, $(x_2, w_2)$ and $(x_3, w_3)$ which are encryptions of $m_1$, $m_2$ and $m_1m_2$, respectively. The random integers used is $r_1$, $r_2$ and $r_3$, respectively. Note that $r_3$ isn't $r_1+r_2$, it is a random number. You want to produce a proof that the encryptions are correct.

The idea is to observe that the ciphertext $(x_1x_2/x_3, w_1 w_2 / w_3)$ is an encryption of $1$. As such, you only need to prove that it is an encryption of $1$. This amounts to proving that the logarithm of $x_1x_2/x_3$ to the base $g$ equals the logarithm of $w_1w_2/w_3$ to the base $y$, which is done using a standard proof of equality of discrete logarithms.

You asked about additively homomorphic cryptosystems, and above I outlined a solution using multiplicative ElGamal. However, the approach works just as well for an additive variant of ElGamal or Paillier.