Low* is a language embedded in F* that can be used as an alternative to C for low-level programming, but inherits F*’s proof and verification capabilities. By using Low* you can write low-level code and prove it correct, all in one language.
KaraMeL (née KreMLin) is the Low* compiler.