A curated set of links to formal methods involving provable code.
This is a curated list of links and resources related to mathematical proofs about the properties of computer programs.
Idris : 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.
Agda : 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.
UR/Web : 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:
Haskell : An advanced, purely functional programming language.
Liquid Haskell : 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)
Elm : 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 no runtime exceptions.
seL4 : The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source. [brochure] [white paper]
Certikos : Certified Kit Operating System.
Compcert : 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. [C compiler]
Bedrock [tutorial pdf] : 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:
HACMS : 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. [more Darpa "formal" tagged links] [verigames-crowdsourced formal verification]
Genode : 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.
The Little Prover The Little Prover introduces inductive proofs as a way to determine facts about computer programs.
Certified Programming with Dependent Types 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. [Latest draft]
Software Foundations by Benjamin Pierce and others. The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
Vol. 1: [read] [download] Logical Foundations, serves as the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving,and Coq.
Vol. 2: [read] [download] Programming Language Foundations, surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
Vol. 3: Verified Functional Algorithms [read] [download] Learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues.
HoTT : Homotopy Type Theory: Univalent Foundations of Mathematics [pdf] 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.
DeepSpec Summer School 41 Videos about deep specification. Coq videos, examples, tutorials.
Adam Chlipala Videos:
2017-12-29 CCC Presentation: Coming Soon Machine-Checked Mathematical Proofs in Everyday Software and Hardware Development
Bedrock: A Software Development Ecosystem Inside a Proof Assistant
CACM August 2016 - Ur/Web: A Simple Model for Programming the Web
2015 Coq Proof Assistant and Its Applications to Programming-Language Semantics
Learning Automated Theorem Proving : Stackexchange post about learning
Curry-Howard : 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".
Hoare logic 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.
Rolf Rolles Program Synthesis in Reverse Engineering ...Assume you generate all possible programs...
The Open-Source seL4 Kernel. Military-Grade Security Through Mathematics - SFO17-417
DARPA Hack Proof Drones Uses SEL4, other RTOS
Hacker-Proof Code Confirmed : 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.
CertiKOS enables creation of secure system kernels [certikos project] 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.
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
seL4 introduction: Capability--based Access Model <- Chinese, translation?
TODO: find Heartbleed Example with Agda Showing Proofs