I work on formal verification of arithmetic circuits, combining computer algebra with SAT solving for word-level reasoning.