|
|
|
|
|
|
by c0balt
75 days ago
|
|
|
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.... and https://lean-lang.org/ (Cedar) |
|
|