My workplace uses Ada SPARK for high-integrity automotive software, ported from C or C++. IIUC, the contracts and static proofs can replace some activities like isolated unit tests for C++ .

https://www.wevolver.com/article/nvidia-adoption-of-spark-us...