In the recent beautiful talk "Motives and ring stacks" Peter Scholze states the theorem saying that there exists an initial 6-functor formalism on $\mathit{Sch}_\mathbb{Z}$ such that
- when $f$ is proper then $f^*$ has a right adjoint $f_*$ that commutes with colimits and satisfies base change + projection formula,
- when $f$ is smooth then $f^*$ has a left adjoint that commutes with limits and satisfies base change and projection formula,
- and satifies the conditions: excision, $\mathbb{A}^1$-invariance and that the Tate twist is invertible.
Scholze cites Gallauer for this theorem, but wasn't this theorem known to Voevodsky and proven by Ayoub in his thesis already in 2007?