Coq
Georges GonthierのチームがSsreflect(small scale reflectionの略)というCoqの拡張を開発している。拡張はreflection用の機能にとどまらず、Coqの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。 Ssreflectの機能には下のようなものがある。
保守性を高めるための機能 Coqが自動生成した識別子をユーザが指定できなくなって、Coqのバージョンアップによって証明が通らなくなることを防止する機能 証明の枝を完結させることを明示して、軽微な証明を自動で行わせられる上に、証明が通らなくなったときに修正するべき範囲がわかりやすくなる機能
主張を直接証明する代わりに、Coq内で検証済みの判定機を実行するreflectionという技法に特化した証明タクティク
有限集合上の和や積などの大きな演算子を扱う機能
代数のライブラリ
SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く。