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

Я бы начал с формального инструмента доказательства, типа Coq или Isabelle, для основной логики. Потом для быстрых проверок свойств использовал бы решатель SMT, например Z3. Для безопасности на низком уровне можно добавить модельную проверку, типа SPIN, а для криптографических гарантий – инструменты вроде ProVerif. Такой набор даёт хороший баланс между строгостью и практичностью.

Документирование доказательств для новичков – это в первую очередь о том, чтобы снизить порог входа, но при этом сохранить строгость. Я бы создал сопроводительный README, в котором объяснил бы процесс верификации, указал на краткое руководство "С чего начать" с минимальным примером, который компилируется и доказывает тривиальное свойство. Затем включил бы скрипты доказательств прямо в репозиторий с понятными комментариями и аннотациями типов, которые служат документацией. Для Coq использовал бы стандартный синтаксис комментариев для объяснения каждого леммы, а для Isabelle полагался бы на заголовки разделов в файлах .thy. И напоследок, настроил бы CI-шаг, который автоматически запускал бы доказательства и публиковал результаты в виде HTML, чтобы читатели могли просматривать дерево доказательств интерактивно. Так доказательства будут и удобочитаемыми для человека, и верифицированными машиной.