Aspects of computing design invariants, by using approximate reachability analysis, include reducing the circuit model for verification and synthesis. Further included is computing invariants using approximate reachability analysis to optimize a circuit model by identifying a plurality of next states for a present state, the plurality of next states capable of being reached from the present state in one transition. The plurality of bits of the next states are compared with a plurality of bits of the present state, and each bit of the present state that is different from at least one next state is changed to variant.