In addition to Coq that other commenters mentioned, there is also a family of proof assistants based on higher-order logic. Isabelle/HOL[1] is probably the most

In addition to Coq that other commenters mentioned, there is also a family of proof assistants based on higher-order logic. Isabelle/HOL[1] is probably the most widely used prover in this family, which also provides a great deal of automation compared to other provers. For example, it has been used to verify the seL4 microkernel [2]. As for introductions to the topic, I can recommend "Concrete Semantics" [3] which introduces the reader to Isabelle/HOL generally and shows how to model semantics of programming language and prove properties about them. For Coq, a widely used book to get started is Software Foundations [4] which is also focused on PL semantics. [1] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ [2] https://sel4.systems/ https://sel4.systems/ [3] http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ [4] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/