Some of Dawson Engler’s work helps solve this problem, starting around [1]. In that, he shows us how to write custom compiler rules in a high-level language. These rules are sufficient to enforce that maybe type. In another paper, Engler (or one of his several talented students, can’t remember now) shows us how to automatically infer many of these rules.

[1] https://web.stanford.edu/~engler/mc-osdi.pdf