Описывается трансформация и верификация программы bus_sort_breadthfirst, принадлежащей ядру ОС Linux и реализующей сортировку устройств, прикрепленных к шине компьютера. Программа трансформируется с языка Си в язык cP с раскрытием макросов, реорганизацией структур и устранением указателей. Далее программа преобразуется на язык функционального программирования WhyML. Для полученной программы строится спецификация и проводится дедуктивная верификация.