Can a type system serve as a proof assistant for foreign functions?
Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom to your theory.

That being said, there are ways. In Coq for instance, there are various formalisations of the C standard (e.g. Robbert Krebbers' work). Because you have an explicit representation of C programs and their semantics, you can write your code directly in the proof assistant and it is then possible to prove some of its properties.