Ghilbert is a format for formal proofs, based on Metamath. It was started by Raph Levien in 2005, and a series of prototypes showed some promise but it never really caught on.
In the fall of 2017, Raph will do a retreat at the Recurse Center, redesigning the language, with a new implementation in Rust.
Watch this space for updates. In the meantime, the following resources are available:
A project of Raph Levien.