Позвольте уточнить -без дополнительного обучения использованию утилиты.
Вот простой пример использования ANSI C Specification Language.
## Код:
```
/*@ 
  ensures \result ==> (*p == m1 * m2);
  ensures \result == (0 <= m1 * m2 <= UINT_MAX); 
*/
bool mult(unsigned *p, unsigned m1, unsigned m2) {
   bool correct = (0 == m2) || ((UINT_MAX / m2) >= m1);
   if (correct) {
      *p = m1 * m2;
   }
   return correct;
}
```

Этот элементарный пример ставит в ступор систему доказательства. Я знаю, как это доказать вручную, но утилите это не поможет. Попробовав разобраться с этим через документацию, я не получил результата. Подумал, что в Ada/SPARK должно быть проще, но там получил то же самое. Нашёл информацию, что есть специальная библиотека, позволяющая доказывать такие вещи, но в свободной поставке я её не нашёл.

Ручного доказательства категорически недостаточно. Перепутает человек названия переменных и не заметит, или совершит любую другую ошибку внимательности. Ручное доказательство будет верным, а программа - нет.