A cohesive ∞-groupoid is formal if all its spaces of k-morphism have infinitesimal extension. If they have first order infinitesimal extension, the formal cohesive -groupoid is an ∞-Lie algebroid.
For the moment see the section Formal cohesive ∞-groupoids at cohesive (∞,1)-topos .
A 1-truncated formal cohesive -groupoid is a formal groupoid. If the space of objects is the terminal object, this is the delooping of a formal group.
More generally, if the space of objects of a formal cohesvive -groupoid is the terminal object, it is the delooping of a formal ∞-group .