A modern proof language
Kind is a minimal proof checker built as a modern proof language for dependent types and formal verification. It is implemented in Haskell and represents a complete rewrite from an earlier JavaScript version. The project is actively developed and maintained, with examples and documentation available in the associated KindBook repository.