Uniqueness of six-functor formalisms [OS Arithmetic Geometry and Representation Theory]