Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?
The Stacks project concerns algebraic (and geometric) stacks - schemes generalised through descent (via sheaves, groupoid fibres etc)