ACL2 turned the Boyer-Moore tradition of automated inductive theorem proving into an executable Common Lisp-based logic that could model and verify commercial hardware and software systems.
Lawrence Paulson designed Isabelle as a generic proof assistant in which different object logics could be represented inside one trusted framework, later developing Isabelle/HOL into a major environment for formal mathematics and verification.
Lean combined a small dependent-type-theory kernel with extensible proof automation and a practical functional programming language, then grew through Mathlib into a major community platform for machine-checked mathematics.
Mike Gordon’s HOL system adapted the LCF trusted-kernel style to higher-order logic and showed that a general logical formalism could be used for practical hardware specification and mechanized verification.