By formal system I mean a language for expressing statements, rules to prove them and usually a reference computer program, which verifies those proofs.

http://us.metamath.org

Probably the simplest system being able to prove all the mathematics one can learn up to high school. Based on principle of rewriting with substitution.

http://mizar.org/

A system with focus on syntax resembling usual mathematical notation.

https://coq.inria.fr/

One of the more modern systems. It is based on intuitionistic approach. It strongly relies on Curry-Howard principle and is a great way to understand that principle. In my opinion, the best source to start learning it is first volume of software foundations.

Correctness of C compiler CompCert was proven with Coq.

DeepSpec is an expedition to formally specify and provide verified implementations for basic computer systems. The subjects covered are C compiler, micro kernel, CPU instruction set and hardware implementation.

Coq has been used to prove some properties of Hedera hash graph algorithm.

Somewhat similar to Coq. Has strong emphasis on automated proof finding.

https://isabelle.in.tum.de/

Correctness of seL4 microkernel was proven with HOL.