AWS has started using it internally recently, but the biggest Lean software project remains Lean 4 itself, which is almost entirely written in Lean 4 (though not verified except for some index operations and data structures). Galois has used Lean 4 internally, too, and I know of another smaller verification project by a German company for verifying some internals that were very difficult to understand.
One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.
One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.