It's faster. Performance usually matters more than security for most "security" products. ;) Having extra code in kernel is usually just asking for it. Here's one done closer to high-assurance principles that I'm sure the WireGuard scheme could be ported to:
Far as keeping it in kernel, it might be implemented in SPARK and Rust to see if it gets through static and dynamic (if necessary) checkers. Test and fuzz it heavily. If C, use strong, static tools to show correctness and/or compiler transformations like SAFEcode (or Softbound+CETS) to immunize it. I know Criswell runs Linux kernel on SVA-OS with SAFEcode but not sure if S+CETS can do it. Such approaches will knock out most of the flaws that lead to code injection.
Maybe most likely, but not necessarily obvious. While there's no popular module for kernel written in something else than C (as far as I know), there are known ways to write working non-C modules.
C was best assumption as 99+% chance it would be C. Yet, you are right in that I've seen device drivers for Linux done in Ada and ATS languages. It's why I usually don't assume but one was warranter here.
http://genode-labs.com/publications/mikro-sina-2005.pdf
Far as keeping it in kernel, it might be implemented in SPARK and Rust to see if it gets through static and dynamic (if necessary) checkers. Test and fuzz it heavily. If C, use strong, static tools to show correctness and/or compiler transformations like SAFEcode (or Softbound+CETS) to immunize it. I know Criswell runs Linux kernel on SVA-OS with SAFEcode but not sure if S+CETS can do it. Such approaches will knock out most of the flaws that lead to code injection.