In Ayoub's thesis, Les six opérations de Grothendieck et le formalisme des cycles évanescents dans le monde motivique (I), Ayoub proved that given a stable homotopical $2$-functor (Definition 1.4.1) $\mathrm{H}:\mathrm{Sch}/S \longrightarrow \mathfrak{TR}$ ($\mathfrak{TR}$: $2$-category of small triangulated categories), then one has a formalism of four operations $(f^*,f_*,f_!,f^!)$ (Scholie 1.4.2). In the proof (which is very long), he has to make an assumption on the category $\mathrm{Sch}/S$ over a base scheme $S$, namely, he considers only quasi-projective $S$-schemes. The reason for doing so is that any morphism inside $\mathrm{Sch}/S$ can be "smoothified", namely, admits a factorization into a closed immersion followed by a smooth morphism.
The difficulty in the proof, as he noted in his ICM2014 talk A guide to ( ́etale) motivic sheaves, is that the category of smoothifications of a morphism is not filtered, in constrast to the category of Nagata compactifications. So the technique is different, in particular, one obtains the well-defined property of proper push-forward $f_!$ before knowing the validity of proper base change (in fact, in his thesis, he proved only the projective base change but one can strengthen this to proper base change by Chow lemma).
So my question is:
How can one remove the quasi-projective assumption? More precisely, how can we move from quasi-projective $S$-schemes to separated $S$-schemes of finite type? Ayoub in loc.cit. noted that the existence of $f^!$ is local on source, so we may reduce to the case of $f$ being quasi-projective, what does he mean by this "local on source"?) Cisinski and Déglise, Triangulated categories of mixed motives seemed to achieve this goal (Theorem 2.4.50). I guess their work relies on Ayoub's thesis but I cannot see the way Ayoub's Scholie 1.4.2 is used in Cisinski & Déglise' book.
Besides, I am interested in proper base change theorem in a greater manner. In the second chapter of his thesis, he defined the so-call notion stable homotopical algebraic derivator and deduced various base change formulas. I wonder whether one can replace "projective" by "proper" in any base change formula of algebraic derivators?