the Nanoda type-checker for Lean is ~5,000 lines of Rust:

https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...

...and for those who are looking to roll-their-own:

https://ammkrn.github.io/type_checking_in_lean4/title_page.h...

...and some thoughts on putting stuff in the kernel:

https://lawrencecpaulson.github.io/2026/07/30/Collatz.html