  Russell is a logical framework for the specification and implementation of
deductive systems. It is a high-level language with respect to Metamath
language, so inherently it uses a Metamath foundations, i.e. it doesn't rely on
any particular formal calculus, but rather is a pure logical framework. The
main difference with Metamath is in the proof language and approach to syntax:
the proofs have a declarative form, i.e. consist of actual expressions, which
are used in proofs, while syntactic grammar rules are separated from the
meaningful rules of inference.
  Russell is implemented in c++14 and is distributed under GPL v3 license. The
repository contains translators from Metamath to Russell and back. Original
Metamath theorem base (almost 30 000 theorems) can be translated to Russell,
verified, translated back to Metamath and verified with the original Metamath
verifier. Russell can be downloaded from the repository
https://github.com/dmitry-vlasov/russell
