Stars
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
The Ott tool for writing definitions of programming languages and calculi
Proof assistant based on the λΠ-calculus modulo rewriting
A proof assistant for higher-dimensional type theory
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
Natty is a natural-language proof assistant with an embedded automatic prover for higher-order logic. It is in an early stage of development.