For me it's a very interesting question whether they directly used the generated C code from the P toolchain in the driver or whether they only used P for verif

For me it's a very interesting question whether they directly used the generated C code from the P toolchain in the driver or whether they only used P for verification of the state machines and reimplemented them in C. Directly using the code would be a huge achievement and can help to avoid a lot of issues that will come with reimplementing it. However it has also quite huge requirements for the code generation. E.g. the scheduler must fit the target system and must be performant for the use-case, the infinite-queue semantics that the state machines seem to have are not ideal for a constrained environment and of course there's questions regarding memory allocation and garbage collection (which should mostly be avoided in drivers).