I know quite a bit about process calculus, although my choice of poison is CSP. The concurrency workbench is CCS, if I remember correctly. FDR, which may be available to developers in academia, handles CSP. Do you know of anything similar for pi-calculus?
You could, of course, follow my PhD thesis and prove a general result about a class of systems and limit yourself to that class of system. You can even write frameworks which make it almost impossible to do anything else. (I could say more but wont.)
Unfortunately whatever you do there is the problem of arguing that the kernel code corresponds to the process calculus or has the things your general proof required.
99.98% of the time concurrency just adds locking and context switches and therefore reduces system performance. The best approach the other 0.02% of the time is a more difficult question.