Languages designed for safety-critical realtime applications do just that. Well, they don't use proofs as proofs generally have a bad cost/benefit ratio (even for sequential programs), but they do use temporal logics that easily deal with concurrency, which they then verify mostly automatically. Temporal logics were introduced to CS in the late '70s, have resulted in at least two Turing awards, and have enjoyed some success in industry.