Ответ 1
Это зависит от того, что вы подразумеваете под "доказательством свойства". Насколько мне известно, существует множество инструментов статического анализа для проверки простых свойств программ на C, и они широко варьируются с точки зрения выразительности, простоты использования, обоснованности анализа и т.д. Они обычно используются для проверки того, что программы бесплатны ошибок во время выполнения, но не очень хороши для проверки полных функциональных спецификаций. Для такого рода свойств вам, возможно, придется прибегнуть к более мощной проверке, которая требует, чтобы вы вручную записали доказательство, вместо того, чтобы автоматически проверять вас.
Поскольку вы упоминаете Coq, я хотел бы направить вас к двум инструментам Coq для проверки программ на C (они не работают с С++, однако): в последней категории есть Verified Software Toolchain, логика для рассуждений о программах на языке C, встроенных внутри Coq. Вы можете использовать его для написания доказательств о поведении вашей программы и проверить их Coq, в том числе показать, что программа соответствует его функциональной спецификации. В предыдущей категории есть Verasco, автоматический инструмент статического анализа, который проверяет вашу программу на отсутствие ошибок во время выполнения. Одна из приятных особенностей этих инструментов заключается в том, что они сами являются проверенными программами, подразумевая, что вы можете получить дополнительную уверенность в анализе, который они предоставляют.
Другие интересные инструменты включают Frama-C, как указано в комментарии выше, и VCC, статический анализатор от Microsoft. Однако они не работают с С++.