Formally verified superblock scheduling. - Cyril Six; Léo Gourdin; Sylvain Boulmé; David Monniaux; Justus Fasse; Nicolas Nardino (CPP, 2022)