[bhy]

I don’t think lean4 compiled code is as efficient as rust. For verification purposes, there are some tools allowing formal verification of rust code.