Proofs of Correctness and Properties of Integer Adder Circuits

Adder circuits have been extensively studied. Their formal properties are well known, but the proofs are either incomplete or difficult to find. This short contribution intends to integrate all formal proofs related to adders in a single place and to add the details when necessary. The presentation is accessible to general VLSI designer. Another goal of this study is to put together relevant materials for the preparation of further formal studies in computer arithmetic. The presentation is made as concise as possible.