Russell — это логический каркас, предназначенный для спецификации и реализации дедуктивных систем. Он является языком высокого уровня по отношению к языку Metamath, поэтому он наследует основания Metamath, то есть не зависит от какого либо конкретного формального исчисления, но является чистым логическим каркасом. Основная разница между Russell и Metamath заключается в языке доказательств и подходу к синтаксису: доказательства в Russell имеют декларативную форму, то есть содержат явно выражения, составляющие доказательство, а синтаксические правила грамматики разделены в Russell с содержательными правилами вывода. Russell реализован на c++14 и распространяется по лицензии GPL v3. Репозиторий содержит транслятор из Metamath в Russell и обратно. Оригинальная база теорем Metamath (почти 30 000 теорем) транслируется в Russell, верифицируется, транслируется обратно в Metamath и верифицируется оригинальным верификатором Metamath. Адрес репозитория: https://github.com/dmitry-vlasov/russell.