Security-related code should be readable and auditable.

Models have gotten good, but c'mon. Good idea, maybe even a good implementation, but I don't have confidence in it, and you've got to have confidence in a project that claims to provide security.

Also, even the best models still regularly write C security bugs. It doesn't make sense to have a model write C code when having it write in a memory safe language is only slightly more effort/cost.