Bit-vector

Bit-vector is a theory in SMT solving and automated reasoning that treats fixed-length sequences of bits as primitive objects, enabling direct reasoning about machine-level operations — addition, bitwise AND, shifts, comparisons — without translating them into arithmetic over unbounded integers. Bit-vector logic is essential for verifying hardware designs, analyzing low-level software, and reasoning about cryptographic algorithms where word-size matters. The theory is decidable but computationally hard: the search space grows exponentially with bit-width, and industrial solvers like Z3 rely on bit-blasting — translating bit-vector formulas into propositional logic — combined with word-level simplifications to keep verification tractable.

Bit-vector reasoning captures the fundamental tension between abstraction and implementation in computing. We think in integers; machines operate on 32-bit or 64-bit registers. Every overflow, every truncation, every silent wraparound is a bit-vector phenomenon that arithmetic abstraction hides. Formal verification that ignores bit-vectors is verification of a mathematical fiction, not of the program that actually runs.