Andrew W. Appel, Princeton University

David Bindel, Cornell University

Geoff Hulette, Sandia National Labs

Ariel Kellison, Cornell University

Josh Cohen, Princeton University

Tim Carstens, RISC Zero

In this collection of research projects, we take a layered approach to foundational verification of correctness and accuracy of numerical software–that is, formal machine-checked proofs about programs (not just algorithms), with no assumptions except specifications of instruction-set architectures. We build, improve, and use appropriate tools at each layer: proving in the real numbers about discrete algorithms; proving how floating-point algorithms approximate real-number algorithms; reasoning about C program implementation of floating-point algorithms; and connecting all proofs end-to-end in Coq.

Our initial research projects (and results) are,



VeriNum’s various projects are supported in part by