I read on the nLab that in "Pursuing stacks" Grothendieck made several interesting conjectures, some of which have been proved since then. For example, as David Roberts wrote in answer to this question,

Grothendieck conjectured, and Cisinski proved, that the class of weak equivalences in the Thomason model structure was the smallest basic localizer.

I am interesting in knowing what other conjectures made in PS have turned out to be true, or other "ideas" that have been successfully realized/formalized. Ideally it would be nice to include references to the relevant papers.