Rocq

Система интерактивного доказательства теорем (proof assistant), раньше называлась Coq. В ней записывают математические доказательства и формальные спецификации программ, а система сама проверяет каждый шаг; из проверенных спецификаций можно автоматически получить рабочий код на OCaml или Haskell. С её помощью сделаны, например, проверенный компилятор языка C CompCert и формальное доказательство теоремы о четырёх красках. Близкий аналог — Lean.

проверено по: rocq-prover.org ↗