Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on

Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?