SampCert

Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a python ffi is used to call into the verified implementation. I don't know if AWS is big enough for your standards, but here is at least one example. Besides that, I'm more reporting on the general vibe I have observed from numerous talks at AI4maths workshops at Neurips, at the DARPA AI4Math ExpMath kickoff, etc. People are considering Lean as a serious programming language. Maybe that's surprising to the mathematicians, but as a PL person, I find the language really nicely designed and I can understand why people want to write in it.

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

HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation that classical logic with simple types enables to a Curry-Howard based prover with dependent types (like Lean, Coq or Adga) is not a fully solved problem. For industrial-scale program verification, proof automation is everything! Nothing else matters. I conjecture, but don't know, that Amazon write their HOL-based prover from scratch, to take into account their cloud resources. So it might well be the most modern prover of all. Note that Leonardo de Moura, who initiated Lean, is now at AWS. To add even more complications, AWS does also use Lean, e.g. https://github.com/leanprover/SampCert