Ha jól értettem: formálisan bizonyították, hogy a forrás szinten nem tartalmaz runtime hibát. Na és a fordítóról bizonyították? A hardverről bizonyították? Stb.