The latest version is Agda. The language it is implementing is Structured Type Theory which is a dependently typed functional language with modern language constructs such as parametrised modules and records. It is quite close to Cayenne. The user can interact with Agda through an emacs-interface, or a graphical interface, Alfa.
We also have a simple web-based proof editor for propositional logic Alfie, which is intended for use in elementary teaching.