Cool, and the paper mentioned in the document "Dependent Types for Low-Level Programming" [1] is such a gem.

[1]: https://people.eecs.berkeley.edu/~necula/Papers/deputy-esop0...