Aya Prover

A proof assistant designed for formalizing math and type-directed programming.