[kevlar700]

There is a podcast and blackhat? video about Nvidia choosing SPARK over Rust. Not because of formal verification at all but because it is a more developed prospect and offers better security even without any formal verification. This isn't mentioned but Ada is also far better at modelling registers or even network packets.

I might consider AI if it utilised SPARKs gnat prove but I wouldn't usw AI otherwise.

[LiamPowell]

As an example of modelling packets, here's an example of modelling a complex packet which is a bit-packed tagged union. I don't think many other languages make such packets so easy to declare: https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...

[xxpor]

p4? Granted, that's not something that just compiles to a usable language.