> First large scale application of proof of correctness technology.

Curious about this. How does it work? Does it use any methods invented by Leslie Lamport?