Dominic Verity and I have been working to develop model independent foundations of $(\infty,1)$-category theory. Our aim at present isn't to cover all models of $(\infty,1)$-categories but only the "best-behaved ones" (which include quasi-categories, complete Segal spaces, Segal categories, and naturally marked simplicial sets). The benefit to restricting to these models is that it allows us to work more strictly so that the development of the basic category theory is more similar to that for ordinary 1-categories, working in the strict 2-category CAT. A survey of the present state of this project can be found here:

$\infty$-category theory from scratch

Let me now sketch how our approach deals with Kan extensions. The details can be found in section 5 of our most recent paper:

Kan extensions and the calculus of modules for $\infty$-categories

For each of the well-behaved models of $(\infty,1)$-categories there is a strict 2-category whose objects are the $(\infty,1)$-categories of this variety, whose morphisms are the $(\infty,1)$-functors, and whose 2-cells I'll call natural transformations. For concision let me now call the objects and morphisms $\infty$-categories and $\infty$-functors. We call this the *homotopy 2-category* because it can be thought of as a categorification of the usual homotopy category associated to a model category. The homotopy 2-categories defined for each of the four models mentioned above are connected by 2-functors that are biequivalences. Each homotopy 2-category has certain additional structures that are derived from a common axiomatization which we use to develop the theory of $\infty$-categories: namely each of the well-behaved models defines what we call an *$\infty$-cosmos*. Everything is proven relative to the $\infty$-cosmos axiomatization, which is why this approach is "model agnostic."

Some pleasant features of the homotopy 2-category is that the equivalences and adjunctions in there are exactly the correct notions, meaning they recover the model-theoretic notions of weak equivalence between $\infty$-categories and also Lurie's notion of adjunctions in the case of quasi-categories (though this isn't obvious). Inside the homotopy 2-category you can also define (co)cartesian fibrations (which again specialize to the Lurie ones in the case of quasi-categories) and also define limits and colimits of diagrams valued in an $\infty$-category indexed by either a simplicial set or by another small $\infty$-category (because the models just mentioned happen to all be cartesian closed).

Now Kan extensions of one $\infty$-functor along another can also be defined in any 2-category but some care is needed here. The universal property of being a mere Kan extension in the homotopy 2-category is not strong enough: instead the correct notion is of a *pointwise Kan extension*. We give two equivalent definitions of this notion but the simplest for the present purpose is that a Kan extension of an $\infty$-functor $f \colon A \to C$ along an $\infty$-functor $k \colon A \to B$ is *pointwise* if when you paste an *exact square* whose bottom edge is $k$ on top, the result is still a Kan extension. Exact squares are squares with a natural transformation in them that are characterized by a property that makes use of the *modules* of the title.

Examples of exact squares include pullback squares one of whose edges is (co)cartesian; perhaps this is the Beck-Chevalley result you were referring to? Another example of an exact square is a comma square. This proves the easy half of the colimit formula for left Kan extensions that you were referring to: the value of the pointwise left Kan extension of $f$ along $k$ at some $b : 1 \to B$ is given by the limit of the restriction of $f$ along the projection $k \downarrow b \to A$.

The converse direction is more subtle because we need to assemble these colimit values, one for each "object" $b$ in $B$, into an $\infty$-functor $lan_k f : B \to C$. What's needed to do this is something like the principle that "universal properties for $\infty$-categories are determined objectwise." For quasi-categories, we prove a precise theorem expressing this idea. The proof involves some horn-filling inductive argument over simplices, so it's very particular to the quasi-categorical model. In the very last part of our paper, we use this to sketch a proof that any cocomplete quasi-category has all Kan extensions of small functors given by the colimit formula (full details will appear in our forthcoming sixth paper, which specializes to the quasi-categorical case).

Because our argument uses the quasi-categorical model there is some model independence lost at this step, but happily it's only lost in the proof, not in the conclusion. The reason for this is a model independence theorem (which is sketched in the "scratch" lecture notes and will be presented in more detail in our forthcoming seventh paper, on model independence). Not only are the homotopy 2-categories for the models mentioned above biequivalent, but there is a more sophisticated categorical structure called a *virtual equipment* that we construct for each model, and these virtual equipments are also biequivalent. The virtual equipment encodes the "calculus of modules" for $\infty$-categories; in particular, this captures the universal properties of cartesian fibrations and Kan extensions and the like. So the "universal properties for $\infty$-categories are determined objectwise" result also holds for the other models and the rest of our argument (which takes place in the virtual equipment) now applies.

Sorry for the length of this post!