Let's see what it takes to trust an F* proof by walking through this proof that 733929337 is the largest truncatable palindromic prime.
Like in any other proof assistant, it requires trusting that the meta-theory of F* is sound. Unlike more mature systems like Coq that have small trusted kernels and independent proof checkers, in the case of F* this entails trusting a larger code base. Mistakes can be made (it has happened in LCF, Coq and F*), but if the author of a proof is well-intended, it's unlikely that they have exploited any unsound corner case to complete a proof. I'm well-intended :)