The reverse-proxies implemented in Rust (aided by Rocq of Rust) in my larger circles were written in-house for their respective platforms. These colleagues fall into the more classical definiton of engineer and "hacker". I know there are some open source reverse-proxies implemented in Rust out there but I am not yet personally familiar with them (by using and supporting them in production) and can't vouch for them.
I agree with xmcp123's comment generally. I know those guys (and some gals) use models for some static analysis of code but they don't use models to generate important code like internet-facing reverse-proxies.
I look forward to the implementations of reverse-proxies in Lean 4 which will be zero-bugs implementations, unless some macro level adjustments need to be made, and may enable the maximum possible utilization of the silicon involved even more so than Rust already does.
If a reverse-proxy implemented in CompCert C could yield some compelling result has been a recent discussion. I'm still personally getting familiar with CompCert C.
Up until the last couple of years from early-ish 2012, I used nginx for production traffic in a lot of places. I have instantiated so many K8s Ingress that were nginx and nginx has been a huge part of my professional and personal life.
Envoy being written in C++ has always given me a gut feeling to avoid Envoy. Aside from occasional SRE-ish support of Envoy (when someone else already instantiated it before I got there), I have successfully avoided it and occasionally successfully displaced Envoy with nginx. I was listening to an Oxide podcast just the other day where bcantrill commented about C++, something along the vibe of waiting for someone still somewhat early along their journey to see the light and move on to Rust.
There will never be a production Rocq of Go and if there ever is, then it wouldn't be the language we call Go today now would it. Go is for flash in the pan stuff that is only meant to.. go so far.