sel4 has a Haskell version that they write before the C (granted, not sure how a ghc generated binary would be verified) but would the problem be tractable in that case?