awesome-awesomeness/html/provable.html

<h1 id="provably-awesome.">Provably Awesome. <a
href="http://awesome.re"><img src="img/badge.svg" /></a></h1>
<p>This is a curated list of links and resources related to mathematical
proofs about the properties of computer programs.</p>
<h4 id="table-of-contents">Table of Contents</h4>
<ul>
<li><a href="#languages">Languages</a> - Languages with good ability to
use formal type safety</li>
<li><a href="#proof-assistants">Proof Assistants</a> - Interactive
theorem provers used to prove properties of programs.</li>
<li><a href="#projects">Projects</a> - Projects involving provably
correct code.</li>
<li><a href="#books">Books</a> - Textbooks commonly referred to</li>
<li><a href="#courses">Courses</a> - Online courses (youtube, university
courses)</li>
<li><a href="#more">More Links</a> - Video presentations about formal
proof of code topics</li>
</ul>
<h2 id="languages">Languages</h2>
<ul>
<li><p><a href="https://www.idris-lang.org/">Idris</a> : Idris is a
general purpose pure functional programming language with dependent
types. Dependent types allow types to be predicated on values, meaning
that some aspects of a program’s behaviour can be specified precisely in
the type. It is compiled, with eager evaluation. Its features are
influenced by Haskell and ML.</p>
<ul>
<li><a href="http://docs.idris-lang.org/en/latest/">Idris docs</a></li>
<li><a
href="http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index">Idris
tutorial</a></li>
<li><a
href="http://docs.idris-lang.org/en/latest/proofs/index.html">Theorem
proving with Idris tutorial</a></li>
</ul></li>
<li><p><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a>
: Dependently typed functional programming language. It has inductive
families, i.e., data types which depend on values, such as the type of
vectors of a given length. It also has parametrised modules, mixfix
operators, Unicode characters, and an interactive Emacs interface which
can assist the programmer in writing the program.</p>
<ul>
<li><a href="https://github.com/agda/agda">Agda Github</a></li>
<li><a href="http://agda.readthedocs.io/en/v2.5.2/">Agda User
Manual</a></li>
</ul></li>
<li><p><a href="http://www.impredicative.com/ur/">UR/Web</a> : Ur/Web is
Ur plus a special standard library and associated rules for parsing and
optimization. Ur/Web supports construction of dynamic web applications
backed by SQL databases. The signature of the standard library is such
that well-typed Ur/Web programs “don’t go wrong” in a very broad sense.
Not only do they not crash during particular page generations, but they
also may not:</p>
<ul>
<li>Suffer from any kinds of code-injection attacks</li>
<li>Return invalid HTML</li>
<li>Contain dead intra-application links</li>
<li>Have mismatches between HTML forms and the fields expected by their
handlers</li>
<li>Include client-side code that makes incorrect assumptions about the
“AJAX”-style services that the remote web server provides</li>
<li>Attempt invalid SQL queries</li>
<li>Use improper marshaling or unmarshaling in communication with SQL
databases or between browsers and web servers</li>
</ul></li>
<li><p><a href="https://www.haskell.org/">Haskell</a> : An advanced,
purely functional programming language.</p></li>
<li><p><a
href="https://ucsd-progsys.github.io/liquidhaskell-blog/">Liquid
Haskell</a> : LiquidHaskell (LH) refines Haskell’s types with logical
predicates that let you enforce critical properties at compile time.
(Guarantee functions are total, keep pointers within bounds, avoid
infinite loops, enforce correctness properties, prove laws by writing
code)</p></li>
<li><p><a href="http://elm-lang.org/">Elm</a> : A type-safe functional
programming language for declaratively creating web browser-based
graphical user interfaces. Implemented in Haskell. It generates
JavaScript with great performance and <em>no runtime
exceptions</em>.</p></li>
</ul>
<h2 id="proof-assistants">Proof Assistants</h2>
<ul>
<li><a href="https://coq.inria.fr/">Coq</a> : Coq is a formal proof
management system. It provides a formal language to write mathematical
definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs.
[<a href="https://coq.inria.fr/download">current stable version</a>] [<a
href="https://coq.inria.fr/distrib/current/refman">reference manual</a>]
<ul>
<li>https://github.com/Ptival/PeaCoq</li>
<li>https://math-comp.github.io/mcb/</li>
</ul></li>
<li><a href="https://isabelle.in.tum.de/">Isabelle</a> : Isabelle is a
generic proof assistant. It allows mathematical formulas to be expressed
in a formal language and provides tools for proving those formulas in a
logical calculus. [<a
href="https://isabelle.in.tum.de/overview.html">overview</a>]</li>
<li><a href="https://hol-theorem-prover.org/">HOL</a> : The HOL
interactive theorem prover is a proof assistant for higher-order logic:
a programming environment in which theorems can be proved and proof
tools implemented. Built-in decision procedures and theorem provers can
automatically establish many simple theorems (users may have to prove
the hard theorems themselves!) An oracle mechanism gives access to
external programs such as SMT and BDD engines. HOL is particularly
suitable as a platform for implementing combinations of deduction,
execution and property checking. [<a
href="https://hol-theorem-prover.org/other-hols.html">Other
HOLS</a>]</li>
<li><a href="https://leanprover.github.io/">LEAN</a> : Lean is a new
open source theorem prover being developed at Microsoft Research, and
its standard library at Carnegie Mellon University. Lean aims to bridge
the gap between interactive and automated theorem proving, by situating
automated tools and methods in a framework that supports user
interaction and the construction of fully specified axiomatic proofs.
The goal is to support both mathematical reasoning and reasoning about
complex systems, and to verify claims in both domains. <a
href="https://leanprover.github.io/live/latest/">Online version</a></li>
<li><a href="http://www.kframework.org/index.php/Main_Page">K
Framework</a> : The K framework is a rewrite-based executable semantic
framework in which programming languages, type systems and formal
analysis tools can be defined using configurations, computations and
rules. Configurations organize the state in units called cells, which
are labeled and can be nested. Computations carry computational meaning
as special nested list structures sequentializing computational tasks,
such as fragments of program. Computations extend the original language
abstract syntax. K (rewrite) rules make it explicit which parts of the
term they read-only, write-only, read-write, or do not care about. This
makes K suitable for defining truly concurrent languages even in the
presence of sharing. Computations are like any other terms in a
rewriting environment: they can be matched, moved from one place to
another, modified, or deleted. This makes K suitable for defining
control-intensive features such as abrupt termination, exceptions or
call/cc.
<ul>
<li><a href="http://www.kframework.org/index.php/K_Tutorial">K
Tutorial</a> by <a href="https://github.com/grosu">Grigore Rosu</a>, <a
href="https://www.youtube.com/watch?v=eSaIKHQOo4c&amp;list=PLx_U8qR-tMtLQEDPvVk1y9gTIdUIWGaQd">video
playlist</a></li>
<li>(https://runtimeverification.com/) : Company formed from K Framework
people. Runtime Verification Inc. is currently developing three core
products:
<ul>
<li>RV-Predict is a predictive runtime analysis tool focused on
automatically detecting concurrency errors in your programs.</li>
<li>RV-Monitor is a development methodology and library generation tool
allowing for the monitoring and enforcement of user-selected properties
at runtime.</li>
<li>RV-Match is a tool allowing for exhaustive runtime verification to
be performed symbolically on all possible program paths, proving certain
properties correct for all possible executions of a given program.</li>
</ul></li>
</ul></li>
<li><a href="https://www.pm.inf.ethz.ch/research/viper.html">Viper</a> :
Viper (Verification Infrastructure for Permission-based Reasoning) is a
language and suite of tools developed at ETH Zurich, providing an
architecture on which new verification tools and prototypes can be
developed simply and quickly. It comprises a novel intermediate
verification language, also named Viper, and automatic verifiers for the
language, as well as example front-end tools. The Viper toolset can be
used to implement verification techniques for front-end programming
languages via translations into the Viper language. ETH Zurich has built
several verifiers on top of Viper, including the <a
href="https://www.pm.inf.ethz.ch/research/gobra.html">Gobra</a> verifier
for Go, <a
href="https://www.pm.inf.ethz.ch/research/nagini.html">Nagini</a> for
Python and <a
href="https://www.pm.inf.ethz.ch/research/prusti.html">Prusti</a> for
Rust.</li>
</ul>
<h2 id="projects">Projects</h2>
<ul>
<li><a href="https://sel4.systems/">seL4</a> : The world’s first
operating-system kernel with an end-to-end proof of implementation
correctness and security enforcement is available as open source. [<a
href="https://sel4.systems/Info/Docs/seL4-brochure.pdf">brochure</a>]
[<a href="https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf">white
paper</a>]</li>
<li><a href="http://flint.cs.yale.edu/certikos/">Certikos</a> :
Certified Kit Operating System.
<ul>
<li><strong>Certified OS Kernels</strong>: Clean-slate design with
end-to-end guarantees on extensibility, security, and resilience.
Without Zero-Day Kernel Vulnerabilities.</li>
<li><strong>Layered Approach</strong>: Divides a complex system into
multiple certified abstraction layers, which are deep specifications of
their underlying implementations.</li>
<li><strong>Languages and Tools</strong>: New formal methods, languages,
compilers and other tools for developing, checking, and automating specs
and proofs.</li>
</ul></li>
<li><a href="http://compcert.inria.fr/">Compcert</a> : The CompCert
project investigates the formal verification of realistic compilers
usable for critical embedded software. Such verified compilers come with
a mathematical, machine-checked proof that the generated executable code
behaves exactly as prescribed by the semantics of the source program.
[<a href="http://compcert.inria.fr/download.html">C compiler</a>]</li>
<li><a href="http://plv.csail.mit.edu/bedrock/">Bedrock</a> [<a
href="http://plv.csail.mit.edu/bedrock/tutorial.pdf">tutorial pdf</a>] :
Bedrock is a library that turns Coq into a tool much like classical
verification systems (e.g., ESC, Boogie), but niftier. In particular,
Bedrock is:
<ul>
<li><strong>Low-level</strong>: You can verify programs that, for
performance reasons or otherwise, can’t tolerate any abstraction beyond
that associated with assembly language.</li>
<li><strong>Foundational</strong>: The output of a Bedrock verification
is a theorem whose statement depends only on the predicates you choose
to use in the key specifications and on the operational semantics of a
simple cross-platform machine language. That is, you don’t need to trust
that the verification framework is bug-free; rather, you need to trust
the usual Coq proof-checker and the formalization of the machine
language semantics.</li>
<li><strong>Higher-order</strong>: Bedrock facilitates quite pleasant
reasoning about code pointers as data.</li>
<li><strong>Computational</strong>: Many useful functions are specified
most effectively by comparing with “reference implementations” in a pure
functional language. Bedrock supports that model, backed by the full
expressive power of Coq’s usual programming language.</li>
<li><strong>Structured</strong>: Bedrock is an extensible programming
language: any client program may add new control flow constructs by
providing their proof rules. For example, adding high-level syntax for
your own calling convention or exception handling construct is
relatively straightforward and does not require tweaking the core
library code.</li>
<li><strong>Mostly automated</strong>: Tactics automate verification
condition generation (in a form inspired by separation logic) and most
of the process of discharging those conditions. Many interesting
programs can be verified with zero manual proof effort, in stark
contrast to most Coq developments.</li>
</ul></li>
<li><dl>
<dt><a
href="https://www.darpa.mil/program/high-assurance-cyber-military-systems">HACMS</a></dt>
<dd>
High-Assurance Cyber Military Systems (HACMS) . Dr. Raymond Richards.
Technology for cyber-physical systems, functionally correct and
satisfying appropriate safety and security properties. Clean-slate,
formal methods, semi-automated code synthesis from executable, formal
specifications. HACMS seeks a synthesizer capable of producing a
machine-checkable proof that generated code satisfies functional specs
as well as security and safety policies, and development to ensure
proofs are composable, allowing components. [<a
href="https://www.darpa.mil/tag-list?tt=78">more Darpa “formal” tagged
links</a>] [<a
href="https://www.darpa.mil/news-events/2013-12-04a">verigames-crowdsourced
formal verification</a>]
</dd>
</dl></li>
<li><a href="http://genode.org/">Genode</a> : Genode is a novel OS
architecture that is able to master complexity by applying a strict
organizational structure to all software components including device
drivers, system services, and applications.</li>
</ul>
<h2 id="books">Books</h2>
<ul>
<li><p><a href="https://mitpress.mit.edu/books/little-prover">The Little
Prover</a> The Little Prover introduces inductive proofs as a way to
determine facts about computer programs.</p></li>
<li><p><a href="http://adam.chlipala.net/cpdt/">Certified Programming
with Dependent Types</a> by Adam Chlipala. Textbook about practical
engineering with the Coq proof assistant. The focus is on building
programs with proofs of correctness, using dependent types and scripted
proof automation. [<a
href="http://adam.chlipala.net/cpdt/cpdt.pdf">Latest draft</a>]</p></li>
<li><p><a href="https://softwarefoundations.cis.upenn.edu/">Software
Foundations</a> by Benjamin Pierce and others. The Software Foundations
series is a broad introduction to the mathematical underpinnings of
reliable software.</p>
<ul>
<li><p><a
href="https://softwarefoundations.cis.upenn.edu/lf-current/index.html">Vol.
1:</a> [<a
href="https://softwarefoundations.cis.upenn.edu/lf-current/toc.html">read</a>]
[<a
href="https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz">download</a>]
Logical Foundations, serves as the entry-point to the series. It covers
functional programming, basic concepts of logic, computer-assisted
theorem proving,and Coq.</p></li>
<li><p><a
href="https://softwarefoundations.cis.upenn.edu/plf-current/index.html">Vol.
2:</a> [<a
href="https://softwarefoundations.cis.upenn.edu/plf-current/toc.html">read</a>]
[<a
href="https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz">download</a>]
Programming Language Foundations, surveys the theory of programming
languages, including operational semantics, Hoare logic, and static type
systems.</p></li>
<li><p><a
href="https://softwarefoundations.cis.upenn.edu/vfa-current/index.html">Vol.
3: Verified Functional Algorithms</a> [<a
href="https://softwarefoundations.cis.upenn.edu/vfa-current/index.html">read</a>]
[<a
href="https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz">download</a>]
Learn how to specify and verify (prove the correctness of) sorting
algorithms, binary search trees, balanced binary search trees, and
priority queues.</p></li>
</ul></li>
<li><p>HoTT : <a href="https://homotopytypetheory.org/book/">Homotopy
Type Theory: Univalent Foundations of Mathematics</a> [<a
href="http://saunders.phil.cmu.edu/book/hott-online.pdfUnivalent">pdf</a>]
Foundations of Mathematics is Vladimir Voevodsky’s new program for a
comprehensive, computational foundation for mathematics based on the
homotopical interpretation of type theory. The type theoretic univalence
axiom relates propositional equality on the universe with homotopy
equivalence of small types. The program is currently being implemented
with the help of the automated proof assistant Coq.</p></li>
<li><p>https://math-comp.github.io/mcb/</p></li>
</ul>
<h2 id="courses">Courses</h2>
<ul>
<li><p><a
href="https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw">DeepSpec
Summer School</a> 41 Videos about deep specification. Coq videos,
examples, tutorials.</p></li>
<li><p>Adam Chlipala Videos:</p>
<ul>
<li><p>2017-12-29 CCC Presentation: <a
href="https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development">Coming
Soon Machine-Checked Mathematical Proofs in Everyday Software and
Hardware Development</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=ORKAy_CHDYM">Adam
Chlipala Lecture 1, OPLSS 2015</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=BSyrp-iYBMo">Bedrock: A
Software Development Ecosystem Inside a Proof Assistant</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=J3XI6-aZZXk">CACM August
2016 - Ur/Web: A Simple Model for Programming the Web</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=yXLeyANzAC4">Proof
engineering Adam Chlipala</a></p></li>
<li><p><a
href="https://www.youtube.com/playlist?list=PLt7hcIEdZLAnO7AawDQkHwE7RtwPDOFEc">2015
Coq Proof Assistant and Its Applications to Programming-Language
Semantics</a></p></li>
</ul></li>
<li><p><a href="https://www.youtube.com/watch?v=X36ye-1x_HQ">Type-Drive
Development in Idris - Edwin Brady</a></p></li>
<li><p><a
href="https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89">Benjamin
Pierce - Software Foundations Course</a></p></li>
<li><p><a
href="https://cs.stackexchange.com/questions/820/learning-automated-theorem-proving">Learning
Automated Theorem Proving</a> : Stackexchange post about
learning</p></li>
</ul>
<h2 id="more">More</h2>
<ul>
<li><p><a
href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard</a>
: Curry–Howard correspondence refers to the direct relationship between
computer programs and mathematical proofs. This is also the idea of
“proofs as programs”, and “propositions (formulas)-as-types”.</p></li>
<li><p><a href="https://en.wikipedia.org/wiki/Hoare_logic">Hoare
logic</a> Hoare logic (also known as Floyd–Hoare logic or Hoare rules)
is a formal system with a set of logical rules for reasoning rigorously
about the correctness of computer programs.</p></li>
<li><p><a
href="https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-192.pdf">Designing
A Theorem Prover (Paulson, Cambridge, 1990)</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=mFjSbxV_1vw">Rolf Rolles
Program Synthesis in Reverse Engineering</a> …Assume you generate all
possible programs…</p></li>
<li><p><a href="https://www.youtube.com/watch?v=heSmrHzHcuM">The
Open-Source seL4 Kernel. Military-Grade Security Through Mathematics -
SFO17-417</a></p></li>
<li><p><a
href="https://www.defensetech.org/2014/05/21/darpa-unveils-hack-proof-drone/">DARPA
Hack Proof Drones</a> Uses SEL4, other RTOS</p></li>
<li><p><a
href="https://www.engadget.com/2015/03/16/pentagon-wants-unhackable-helicopters/">Pentagon
Wants Unhackable Helicopters</a></p></li>
<li><p><a
href="https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/">Hacker-Proof
Code Confirmed</a> : Computer scientists can prove certain programs to
be error-free with the same certainty that mathematicians prove
theorems. The advances are being used to secure everything from unmanned
drones to the internet.</p></li>
<li><p><a
href="http://www.zdnet.com/article/certikos-a-hacker-proof-os/">CertiKOS
enables creation of secure system kernels</a> [<a
href="http://flint.cs.yale.edu/certikos/">certikos project</a>] Computer
system security stinks, because our software is buggy and untestable in
full. Great for cyber criminals, but not for us. So why doesn’t someone
build a mathematically verified, secure, concurrent kernel that can run
on x86 and ARM? A team at Yale has.</p></li>
<li><p><a href="https://www.youtube.com/watch?v=lRndE7rSXiI">seL4 Is
Free – What Does This Mean For You?</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=RdoaFc5-1Rk">From L3 to
seL4 what have we learnt in 20 years of L4 microkernels?</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=x3P6Y6VO0UI">seL4
introduction: Capability–based Access Model</a> &lt;- Chinese,
translation?</p></li>
<li><p><a
href="https://www.youtube.com/playlist?list=PL8UO9ZG39Nx43YCAKGCtj9Rb6p2_3utdc">seL4
playlist</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=4oONdV5RYp8">Creating
drones that can’t be hacked</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=OyqNpn6JpBk">HACMS:
Protecting Military Systems from Hackers</a></p></li>
<li><p><a href="https://www.youtube.com/watch?v=tRtK4xOK-8o">Formal
Methods for Avionics Software Verification pt1</a></p></li>
<li><p>TODO: find Heartbleed Example with Agda Showing Proofs</p></li>
</ul>