SCADE - из INRIA уши растут, SPARK на ихнем движке работает, язычок F* на котором я примеры как раз приводил - сопродукция MS Research и INRIA (щас ушел полностью под INRIA), И кстати казавшийся мне странным их выбор проектов на деле совершенно логичен и даже довольно прикладного свойства.
Совершенно не удивлюсь если окажется что спонсируют все это EADS и Areva с лягушачьим министерством обороны на паях. Точнее довольно сильно удивлюсь если это не так.
И кстати особенности эволюции OCaml ясны - он под конкретные задачи на сам деле развивается
PS: Coq кстати тоже давно уже не только абстрактная формализация математики, а один из самых мощных движков под это дело (в принципе тот же why3 может и его использовать) - просто как я понимаю для end-user-овского продукта сложноват в использовании
Xavier Leroy кстати занимается щас compcert - полностью верифицированным компилятором С (сейчас утверждается, что на 90% примерно) - тоже когда первый раз узнал очень удивился - а сейчас все на свои места тоже стало
