I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. The

I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool. The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation. [0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Big.20news.20from.20Amazon.20Web.20Services.html https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ https://lean-lang.org/ (Cedar)