Perga is a WIP basic proof assistant based on the calculus of constructions. It exists almost exclusively as a project for me to improve my understanding of type theory, though it is a surprisingly competent proof assistant, at least as competent as Automath.