Платформа

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

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

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