Formal verification using computer algebra has emerged as a powerful approach for circuit verification. This technique encodes a circuit, represented as an and-inverter graph, into a set of polynomials that generates a Gröbner basis. Verification relies on computing the polynomial remainder of the specification. But there is a catch: a monomial blow-up often occurs during specification rewriting — a problem that often necessitates dedicated heuristics to manage the complexity. In the first part of the talk, I will provide an introduction to arithmetic circuit verification and discuss how computer algebra can be used in this setting. In the second part, I will present a novel approach, which shifts the computational effort to rewriting the Gröbner basis itself rather than the specification. By restructuring the basis to include linear polynomials, we tame the monomial blow-up and simplify the rewriting process.