Prototyping a Scalable Proof Engine

Prototyping a Scalable Proof Engine Author(s) Rosario, JonAdvisor Chlipala, Adam Terms of use Abstract Formal verification is an exciting development in software engineering, enabling implementations of programs to be rigorously checked against mathematical specifications. Assuming the specification is well-defined, formal verification provides guarantees of a program’s correctness and freedom from bugs that are simply not possible with test-based methods. There’s just one catch: the process of.