Axiom Math рассматривает частичную формальную верификацию как инструмент оптимизации ПО

Axiom Math рассматривает формальную верификацию не только как защиту от ошибок, но и как инструмент повышения производительности и оптимизации. По оценке компании, снижение стоимости формальных доказательств может способствовать созданию новых алгоритмов и научных открытий, а также иметь последствия для программирования, ИИ для науки и физической инженерии.

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