I was surprised to discover recently that C++ is in a pretty nice sweet spot for verification (at least at the binary level), where it has some useful type system features, but will get out of your way and generate simple ASM (without e.g. spamming bounds checks and panics everywhere as rust does).