Здравствуйте, dilettante, Вы писали:

D>Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете?
D>Интересует возможность практического применения.

Один из авторов Nemerle — Michał Moskal:
http://research.microsoft.com/en-us/um/people/moskal/
сейчас работает именно над таким проектом (VCC) в рамках Microsoft Research и какой-то там матери.
Насколько я знаю уже применяют на практике.

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