[johnisgood]

Ada has built-in constructs for concurrency, with contracts, and there is formal verification in a subset of Ada named SPARK, so Ada / SPARK is pretty good.