4 ms·
"I wonder how they formally verify that. " They might be using a different definition of formally verify than you think. SPARK is one of the "lightweight" meth
by nickpsecurity 9y ago
"I wonder how they formally verify that. "
They might be using a different definition of formally verify than you think. SPARK is one of the "lightweight" methods that tries to automate a lot of stuff with the rest hand-proven. They might just mean it's formally verified to not have all the common code injections since SPARK can do that with a good deal automated vs manual proof. Full correctness of that operation would be something different they might need a proof assistant for or considerable effort.
An example of one doing full, formal verification of all kinds of components is CertiKOS at DeepSpec:
http://deepspec.org/ http://deepspec.org/
http://flint.cs.yale.edu/certikos/ http://flint.cs.yale.edu/certikos/