  The Cartan formula encodes the relationship between the cup product and the
action of the Steenrod algebra in $\mathbb F_p$-cohomology. In this work, we
present an effective proof of the Cartan formula at the cochain level when the
field is $\mathbb F_2$. More explicitly, for an arbitrary pair of cocycles and
any non-negative integer, we construct a natural coboundary that descends to
the associated instance of the Cartan formula. Our construction works for
general algebras over the Barratt-Eccles operad, in particular, for the
singular cochains of spaces.
