Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).