  We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR)
decision procedure for first-order real arithmetic in Isabelle/HOL. BKR's
algorithm has good potential for parallelism and was designed to be used in
practice. Its key insight is a clever recursive procedure that computes the set
of all consistent sign assignments for an input set of univariate polynomials
while carefully managing intermediate steps to avoid exponential blowup from
naively enumerating all possible sign assignments (this insight is fundamental
for both the univariate case and the general case). Our proof combines ideas
from BKR and a follow-up work by Renegar that are well-suited for
formalization. The resulting proof outline allows us to build substantially on
Isabelle/HOL's libraries for algebra, analysis, and matrices. Our main
extensions to existing libraries are also detailed.
