F* is a programming language as well as a proof-assistant putting a strong emphasis on practical verification of effectful programs. In order to enable the verification of security critical programs such as cryptographic primitives (HACL) or protocols (TLS in MiTLS), F provides a rich logic with dependent types and universes, an effect-based weakest precondition calculus and an smt-automation backend. In this presentation, we will present how these ingredients are used in actual program verification and then give an account of their metatheoretical aspects.