This would be important because even if you have proven the functional correctness of a kernel, that typically excludes the concurrency aspect.
Like one thing it already gets wrong is that you can send mutable pointers around without clear ownership.
Which Lisps are you thinking of? CL and Scheme both allow having multiple copies of mutable objects.
You can compose small systems, even with multiple parties, prove they cannot deadlock, then make them a 'black box' with defined IO, and build larger, more complex systems with equal properties.
The downside is you must guard every piece of shared data with a separate thread, but there may be ways to reduce the performance penalty.