Cedar (https://lean-lang.org/use-cases/cedar/) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their approach is compelling.

The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or source or random inputs. Then you can explore a lot of the state space fully automatically.

In addition to Cedar:

[1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust.

[2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they use pure Lean functions and interface with C code across the FFI.

[3] SampCert (AWS). Verified random sampling algorithms for differential privacy. Uses pure Lean functions and is called into via the reverse FFI.

Full disclosure I worked on 2 and 3 haha. There's also some stuff being used by cryptocurrency people but I don't follow that very closely.

[1] https://www.microsoft.com/en-us/research/blog/rewriting-symc... [2] https://github.com/leanprover/KLR [3] https://github.com/leanprover/SampCert