Для программных систем необходимо аппаратное обеспечение — компьютер, массово используемые аппаратные платформы, скорее всего, нельзя применять для обсуждаемых задач, т. к. при их разработке приоритет отдаётся производительности (и это не идёт на пользу надёжности, судя по найденным уязвимостям в популярных процессорах), а общественным системам важнее надёжность. Поэтому будет необходимо выбрать или разработать надёжную аппаратную платформу, пригодную для верификации, пусть даже и менее производительную.

Аналогичная ситуация и с операционной системой — в данных задачах важны не универсальность и производительность, а надёжность, поэтому популярные варианты вряд ли подойдут, хотя возможно применение существующих верифицированных микроядер вроде seL4.

Скорее всего, также будет необходимо выбрать язык программирования для разработки всего программного обеспечения исходя из заданных критериев. Вполне возможно, что для упрощения и надёжности аппаратная платформа должна быть спроектирована для выполнения программ на этом языке, однако обсуждение технических деталей уже выходит за рамки данной книги.