We describe the results and status of a project aiming to provide a provably
correct library of basic circuits. We use the theorem proving system PVS
in order to prove circuits such as incrementers, adders, arithmetic units,
multipliers, leading zero counters, shifters, and decoders.
All specifications and proofs are available on the web.