We will describe a version of Grothendieck's 6-functor formalism using the (∞,2)-category of correspondences (aka spans). Namely, this formalism is given as a functor from an appropriate category of correspondences to the category of categories. We will describe several universal properties of this (∞,2)-category and use them to construct such functors. Along the way, we consider ∞-versions of 2-categorical notions such as double categories and the lax Gray tensor product. This is joint work with Dennis Gaitsgory.