Can a type system serve as a proof assistant for foreign functions?

Question

Given that:

1. A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO.
2. There are proof assistants that can be used to prove some properties of a program written in a language that doesn't have a type system capable of expressing those properties.
3. The Curry–Howard correspondence shows that a successfully type-checked implementation of a function with a given type is proof of what is expressed by that type.

Can one express non-trivial proofs of some property of foreign language code in the type system of the native language?

For example, pretend I have a C function called stable_qsort that sorts numbers in a terribly clever and efficient way while maintaining the order of already equal elements, and an Idris program that calls stable_qsort via its FFI, but I don't trust this relatively obscure C function. Could I prove that the function doesn't reorder equal elements, for all inputs, in my Idris code instead of using a separate proof assistant?