In the definition of the crystalline site, there are some nilpotent PD thickenings around. If you replace those by $p$-complete PD thickenings (so that modulo every $p^n$ you get a nilpotent PD thickening as before), you get a site that directly computes the limit over $n$ of crystalline cohomology modulo $p^n$. Is that what you are asking?

Re "hard: I wasn't able to give a slick presentation of the usual proper base change theorem in etale cohomology (a proof would seem to require a further digression), so I'd consider that "hard".

@D.-C.Cisinski About "constructing $f_!$ vs proving that it exists": In the construction principle I explain in lecture 4 of my notes, the functor $f_!$ is not additional data; rather its existence is really a proposition (in the HTT sense, if you want). I agree that the verification of the assumptions becomes the hard part, but that part is not anymore a construction (i.e., you don't have to supply any data), it's just proving a theorem. And let's see how me writing the notes goes, but I think it won't really be hard either.

Due to ignorance, let me not say anything.

@Z.M Regarding your first comment: Yes, I think one could also set up this using the infinitesimal site (in characteristic 0), or the de Rham stack (which is essentially the same story), or also with solid modules (where one can treat formal completions differently, and accordingly gets a slightly different theory). I'm still a bit confused about the relations between all possible choices (I'm just learning about D-modules...), I hope to clear this up for myself while writing the notes...

(By the way, when referring to it as Mann's definition, I'm aware that closely related definitions have been around (Liu-Zheng, Gaitsgory-Rozenblyum, etc), but as far as I'm aware Mann was the first to pin down this precise definition, which at least for my concerns is the "best" among many closely related definitions.)

@D.-C.Cisinski I'm a bit confused by your answer. Most importantly, in Lucas Mann's construction principle, you don't have to construct $f_!$, you just check that it exists. Often the only nontrivial step is to check proper base change. I plan to write up some notes on $D$-modules for my course; I think one can give fairly direct proofs (not having to rely on hard theorems). Also, six functors as in Mann's definition don't have to satisfy excision, $\mathbb A^1$-invariance or cdh-descent, which is good as coherent sheaves don't.

That said, there is definitely room for some kind of algorithm or graphical calculus or such that would help one check expected commutative diagrams involving all six functors.

I'm not sure what a "theorem" justifying the assertion would be, as the "classical" notion of a 6-functor-formalism is somewhat ill-defined, consisting of some slightly random collection of expected isomorphisms, coherences, and maps.

What I meant is just that passing to adjoint functors has extremely good functoriality properties (they are unique up to contractible choice and "functorial"), and that all the "formulas" one knows that involve some of those right adjoints can be deduced (like $f^! Hom(A,B)=Hom(f^*A,f^!B)$). So far I have not seen expected coherences that did not follow automatically from the given datum. This includes, notably, the identifications $f^!=f^*$ for etale $f$, and $f_!=f_*$ for proper $f$ (as well as the map $f_!\to f_*$ for separated $f$).