Eddie
Eddie is an editor of Mizar articles.
Currently it's available in two versions: for Mizar and for Mizar-MSE.
In the second case, the program also includes the checker - the module responsible for verifying proof correctness.
Mizar-MSE Syntax
Descriptions of all reserved words in Mizar-MSE, with examples of usage.
Mizar
