[38;5;12m                                                                                         [39m[38;2;255;187;0m[1m[4mProvably Awesome.    [0m[38;5;14m[1m[4m![0m[38;5;14m[1m[4m (img/badge.svg)[0m[38;2;255;187;0m[1m[4m (http://awesome.re)[0m

[38;5;12mThis is a curated list of links and resources related to mathematical proofs[39m
[38;5;12mabout the properties of computer programs.[39m

[38;2;255;187;0m[4mTable of Contents[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLanguages[0m[38;5;12m (#languages) - Languages with good ability to use formal type[39m
[38;5;12msafety[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mProof Assistants[0m[38;5;12m (#proof-assistants) - Interactive theorem provers used to[39m
[38;5;12mprove properties of programs.[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mProjects[0m[38;5;12m (#projects) - Projects involving provably correct code.[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mBooks[0m[38;5;12m (#books) - Textbooks commonly referred to [39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCourses[0m[38;5;12m (#courses) - Online courses (youtube, university courses)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mMore Links[0m[38;5;12m (#more) - Video presentations about formal proof of code topics[39m

[38;2;255;187;0m[4mLanguages[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mIdris[0m[38;5;12m (https://www.idris-lang.org/) : Idris is a general purpose pure [39m
[38;5;12mfunctional programming language with dependent types. Dependent types allow [39m
[38;5;12mtypes to be predicated on values, meaning that some aspects of a program’s [39m
[38;5;12mbehaviour can be specified precisely in the type. It is compiled, with eager [39m
[38;5;12mevaluation. Its features are influenced by Haskell and ML.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mIdris docs[0m[38;5;12m (http://docs.idris-lang.org/en/latest/)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mIdris tutorial[0m[38;5;12m (http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mTheorem proving with Idris tutorial[0m[38;5;12m (http://docs.idris-lang.org/en/latest/proofs/index.html)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mAgda[0m[38;5;12m (http://wiki.portal.chalmers.se/agda/pmwiki.php) : Dependently[39m
[38;5;12m typed functional programming language. It has inductive families, i.e., data [39m
[38;5;12m types which depend on values, such as the type of vectors of a given length. [39m
[38;5;12m It also has parametrised modules, mixfix operators, Unicode characters, and an[39m
[38;5;12m  interactive Emacs interface which can assist the programmer in writing the [39m
[38;5;12m  program.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mAgda Github[0m[38;5;12m (https://github.com/agda/agda)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mAgda User Manual[0m[38;5;12m (http://agda.readthedocs.io/en/v2.5.2/)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mUR/Web[0m[38;5;12m (http://www.impredicative.com/ur/) : Ur/Web is Ur plus a special [39m
[38;5;12mstandard library and associated rules for parsing and optimization. Ur/Web [39m
[38;5;12msupports construction of dynamic web applications backed by SQL databases. [39m
[38;5;12mThe signature of the standard library is such that well-typed Ur/Web programs [39m
[38;5;12m"don't go wrong" in a very broad sense. Not only do they not crash during [39m
[38;5;12mparticular page generations, but they also may not:[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mSuffer from any kinds of code-injection attacks[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mReturn invalid HTML[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mContain dead intra-application links[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mHave mismatches between HTML forms and the fields expected by their handlers[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mInclude client-side code that makes incorrect assumptions about the [39m
[48;5;235m[38;5;249m"AJAX"-style services that the remote web server provides[49m[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mAttempt invalid SQL queries[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mUse improper marshaling or unmarshaling in communication with SQL databases[39m
[48;5;235m[38;5;249mor between browsers and web servers[49m[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHaskell[0m[38;5;12m (https://www.haskell.org/) : An advanced, purely functional [39m
[38;5;12mprogramming language. [39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLiquid Haskell[0m[38;5;12m (https://ucsd-progsys.github.io/liquidhaskell-blog/) :[39m
[38;5;12mLiquidHaskell (LH) refines Haskell's types with logical predicates that let [39m
[38;5;12myou enforce critical properties at compile time. (Guarantee functions are total,[39m
[38;5;12mkeep pointers within bounds, avoid infinite loops, enforce correctness [39m
[38;5;12mproperties, prove laws by writing code)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mElm[0m[38;5;12m (http://elm-lang.org/) : A type-safe functional programming language for [39m
[38;5;12mdeclaratively creating web browser-based graphical user interfaces. [39m
[38;5;12mImplemented in Haskell. It generates JavaScript with great performance and [39m
[48;2;30;30;40m[38;5;13m[3mno runtime exceptions[0m[38;5;12m.[39m

[38;2;255;187;0m[4mProof Assistants[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCoq[0m[38;5;12m (https://coq.inria.fr/) : Coq is a formal proof management system. It [39m
[38;5;12mprovides a formal language to write mathematical definitions, executable [39m
[38;5;12malgorithms and theorems together with an environment for semi-interactive [39m
[38;5;12mdevelopment of machine-checked proofs. [39m
[38;5;12mcurrent stable version[39m[38;5;14m[1m (https://coq.inria.fr/download)[0m[38;5;12m [39m
[38;5;12mreference manual[39m[38;5;14m[1m (https://coq.inria.fr/distrib/current/refman)[0m[38;5;12m [39m
[48;5;235m[38;5;249m* https://github.com/Ptival/PeaCoq[49m[39m
[48;5;235m[38;5;249m* https://math-comp.github.io/mcb/[49m[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mIsabelle[0m[38;5;12m (https://isabelle.in.tum.de/) : Isabelle is a generic proof assistant.[39m
[38;5;12m It allows mathematical formulas to be expressed in a formal language and [39m
[38;5;12m provides tools for proving those formulas in a logical calculus.[39m
[38;5;12m [39m[38;5;12moverview[39m[38;5;14m[1m (https://isabelle.in.tum.de/overview.html)[0m[38;5;12m [39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHOL[0m[38;5;12m (https://hol-theorem-prover.org/) : The HOL interactive theorem prover is[39m
[38;5;12m a proof assistant for higher-order logic: a programming environment in which [39m
[38;5;12m theorems can be proved and proof tools implemented. Built-in decision [39m
[38;5;12m procedures and theorem provers can automatically establish many simple [39m
[38;5;12m theorems (users may have to prove the hard theorems themselves!) An oracle [39m
[38;5;12m mechanism gives access to external programs such as SMT and BDD engines. [39m
[38;5;12m HOL is particularly suitable as a platform for implementing combinations of [39m
[38;5;12m deduction, execution and property checking. [39m
[38;5;12m [39m[38;5;12mOther HOLS[39m[38;5;14m[1m (https://hol-theorem-prover.org/other-hols.html)[0m[38;5;12m [39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLEAN[0m[38;5;12m (https://leanprover.github.io/) : Lean is a new open source theorem [39m
[38;5;12m prover being developed at Microsoft Research, and its standard library at [39m
[38;5;12m Carnegie Mellon University. Lean aims to bridge the gap between interactive and [39m
[38;5;12m automated theorem proving, by situating automated tools and methods in a framework [39m
[38;5;12m that supports user interaction and the construction of fully specified axiomatic [39m
[38;5;12m proofs. The goal is to support both mathematical reasoning and reasoning about [39m
[38;5;12m complex systems, and to verify claims in both domains.[39m
[38;5;12m   [39m[38;5;14m[1mOnline version[0m[38;5;12m (https://leanprover.github.io/live/latest/)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mK Framework[0m[38;5;12m (http://www.kframework.org/index.php/Main_Page) : The K framework[39m
[38;5;12m is a rewrite-based executable semantic framework in which programming languages, [39m
[38;5;12m type systems and formal analysis tools can be defined using configurations, [39m
[38;5;12m computations and rules. Configurations organize the state in units called cells, [39m
[38;5;12m which are labeled and can be nested. Computations carry computational meaning as [39m
[38;5;12m special nested list structures sequentializing computational tasks, such as fragments [39m
[38;5;12m of program. Computations extend the original language abstract syntax. K (rewrite) [39m
[38;5;12m rules make it explicit which parts of the term they read-only, write-only, read-write, [39m
[38;5;12m or do not care about. This makes K suitable for defining truly concurrent languages [39m
[38;5;12m even in the presence of sharing. Computations are like any other terms in a rewriting [39m
[38;5;12m environment: they can be matched, moved from one place to another, modified, or [39m
[38;5;12m deleted. This makes K suitable for defining control-intensive features such as [39m
[38;5;12m abrupt termination, exceptions or call/cc.[39m
[38;5;12m [39m[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mK Tutorial[0m[38;5;12m (http://www.kframework.org/index.php/K_Tutorial) by [39m[38;5;14m[1mGrigore Rosu[0m[38;5;12m (https://github.com/grosu), [39m[38;5;14m[1mvideo playlist[0m[38;5;12m (https://www.youtube.com/watch?v=eSaIKHQOo4c&list=PLx_U8qR-tMtLQEDPvVk1y9gTIdUIWGaQd)[39m
[38;5;12m [39m[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12m(https://runtimeverification.com/) : Company formed from K Framework people. [39m
[48;5;235m[38;5;249m Runtime Verification Inc. is currently developing three core products: [49m[39m[48;5;235m[38;5;249m           [49m[39m
[48;5;235m[38;5;249m * RV-Predict is a predictive runtime analysis tool focused on automatically [49m[39m[48;5;235m[38;5;249m      [49m[39m
[48;5;235m[38;5;249m   detecting concurrency errors in your programs. [49m[39m[48;5;235m[38;5;249m                                 [49m[39m
[48;5;235m[38;5;249m * RV-Monitor is a development methodology and library generation tool allowing [49m[39m[48;5;235m[38;5;249m   [49m[39m
[48;5;235m[38;5;249m   for the monitoring and enforcement of user-selected properties at runtime. [49m[39m[48;5;235m[38;5;249m     [49m[39m
[48;5;235m[38;5;249m * RV-Match is a tool allowing for exhaustive runtime verification to be performed [49m[39m
[48;5;235m[38;5;249m   symbolically on all possible program paths, proving certain properties correct [49m[39m[48;5;235m[38;5;249m [49m[39m
[48;5;235m[38;5;249m   for all possible executions of a given program.[49m[39m[48;5;235m[38;5;249m                                 [49m[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mViper[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/viper.html)[39m[38;5;12m [39m[38;5;12m:[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12m(Verification[39m[38;5;12m [39m[38;5;12mInfrastructure[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPermission-based[39m[38;5;12m [39m[38;5;12mReasoning)[39m[38;5;12m [39m[38;5;12mis[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mlanguage[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12msuite[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mtools[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12mat[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich,[39m[38;5;12m [39m[38;5;12mproviding[39m[38;5;12m [39m[38;5;12man[39m[38;5;12m [39m[38;5;12marchitecture[39m[38;5;12m [39m[38;5;12mon[39m[38;5;12m [39m[38;5;12mwhich[39m[38;5;12m [39m[38;5;12mnew[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m
[38;5;12mtools[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mprototypes[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m[38;5;12mdeveloped[39m[38;5;12m [39m[38;5;12msimply[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mquickly.[39m[38;5;12m [39m[38;5;12mIt[39m[38;5;12m [39m[38;5;12mcomprises[39m[38;5;12m [39m[38;5;12ma[39m[38;5;12m [39m[38;5;12mnovel[39m[38;5;12m [39m[38;5;12mintermediate[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12malso[39m[38;5;12m [39m[38;5;12mnamed[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;12mautomatic[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mlanguage,[39m[38;5;12m [39m[38;5;12mas[39m[38;5;12m [39m[38;5;12mwell[39m[38;5;12m [39m[38;5;12mas[39m[38;5;12m [39m[38;5;12mexample[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mtools.[39m[38;5;12m [39m[38;5;12mThe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mtoolset[39m[38;5;12m [39m[38;5;12mcan[39m[38;5;12m [39m[38;5;12mbe[39m[38;5;12m [39m
[38;5;12mused[39m[38;5;12m [39m[38;5;12mto[39m[38;5;12m [39m[38;5;12mimplement[39m[38;5;12m [39m[38;5;12mverification[39m[38;5;12m [39m[38;5;12mtechniques[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mfront-end[39m[38;5;12m [39m[38;5;12mprogramming[39m[38;5;12m [39m[38;5;12mlanguages[39m[38;5;12m [39m[38;5;12mvia[39m[38;5;12m [39m[38;5;12mtranslations[39m[38;5;12m [39m[38;5;12minto[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;12mViper[39m[38;5;12m [39m[38;5;12mlanguage.[39m[38;5;12m [39m[38;5;12mETH[39m[38;5;12m [39m[38;5;12mZurich[39m[38;5;12m [39m[38;5;12mhas[39m[38;5;12m [39m[38;5;12mbuilt[39m[38;5;12m [39m[38;5;12mseveral[39m[38;5;12m [39m[38;5;12mverifiers[39m[38;5;12m [39m[38;5;12mon[39m[38;5;12m [39m[38;5;12mtop[39m[38;5;12m [39m[38;5;12mof[39m[38;5;12m [39m[38;5;12mViper,[39m[38;5;12m [39m[38;5;12mincluding[39m[38;5;12m [39m[38;5;12mthe[39m[38;5;12m [39m[38;5;14m[1mGobra[0m[38;5;12m [39m
[38;5;12m(https://www.pm.inf.ethz.ch/research/gobra.html)[39m[38;5;12m [39m[38;5;12mverifier[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mGo,[39m[38;5;12m [39m[38;5;14m[1mNagini[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/nagini.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mPython[39m[38;5;12m [39m[38;5;12mand[39m[38;5;12m [39m[38;5;14m[1mPrusti[0m[38;5;12m [39m[38;5;12m(https://www.pm.inf.ethz.ch/research/prusti.html)[39m[38;5;12m [39m[38;5;12mfor[39m[38;5;12m [39m[38;5;12mRust.[39m

[38;2;255;187;0m[4mProjects[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mseL4[0m[38;5;12m (https://sel4.systems/) : The world's first operating-system kernel with [39m
[38;5;12man end-to-end proof of implementation correctness and security enforcement [39m
[38;5;12mis available as open source. [39m
[38;5;12mbrochure[39m[38;5;14m[1m (https://sel4.systems/Info/Docs/seL4-brochure.pdf)[0m[38;5;12m [39m
[38;5;12mwhite paper[39m[38;5;14m[1m (https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf)[0m[38;5;12m [39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCertikos[0m[38;5;12m (http://flint.cs.yale.edu/certikos/) : Certified Kit Operating [39m
[38;5;12mSystem.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCertified OS Kernels[0m[38;5;12m: Clean-slate design with end-to-end guarantees on [39m
[48;5;235m[38;5;249mextensibility, security, and resilience.[49m[39m
[48;5;235m[38;5;249mWithout Zero-Day Kernel Vulnerabilities.[49m[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLayered Approach[0m[38;5;12m: Divides a complex[39m
[48;5;235m[38;5;249m system into multiple certified abstraction layers, which are deep [49m[39m
[48;5;235m[38;5;249m specifications of their underlying implementations.[49m[39m[48;5;235m[38;5;249m               [49m[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLanguages and Tools[0m[38;5;12m: New formal methods, languages, compilers and other [39m
[38;5;12m  tools for developing, checking, and automating specs and proofs.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCompcert[0m[38;5;12m (http://compcert.inria.fr/) : The CompCert project investigates the [39m
[38;5;12mformal verification of realistic compilers usable for critical embedded [39m
[38;5;12msoftware. Such verified compilers come with a mathematical, machine-checked [39m
[38;5;12mproof that the generated executable code behaves exactly as prescribed by the [39m
[38;5;12msemantics of the source program. [39m
[38;5;12mC compiler[39m[38;5;14m[1m (http://compcert.inria.fr/download.html)[0m[38;5;12m [39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mBedrock[0m[38;5;12m (http://plv.csail.mit.edu/bedrock/) [39m
[38;5;12mtutorial pdf[39m[38;5;14m[1m (http://plv.csail.mit.edu/bedrock/tutorial.pdf)[0m[38;5;12m  :[39m
[38;5;12mBedrock is a library that turns Coq into a tool much like classical [39m
[38;5;12mverification systems (e.g., ESC, Boogie), but niftier. In particular, [39m
[38;5;12mBedrock is:[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLow-level[0m[38;5;12m: You can verify programs that, for performance reasons or [39m
[38;5;12m  otherwise, can't tolerate any abstraction beyond that associated with [39m
[38;5;12m  assembly language.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mFoundational[0m[38;5;12m: The output of a Bedrock verification is a theorem whose [39m
[38;5;12m  statement depends only on the predicates you choose to use in the key [39m
[38;5;12m  specifications and on the operational semantics of a simple cross-platform [39m
[38;5;12m  machine language. That is, you don't need to trust that the verification [39m
[38;5;12m  framework is bug-free; rather, you need to trust the usual Coq proof-checker[39m
[38;5;12m  and the formalization of the machine language semantics.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHigher-order[0m[38;5;12m: Bedrock facilitates quite pleasant reasoning about code [39m
[38;5;12m  pointers as data.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mComputational[0m[38;5;12m: Many useful functions are specified most effectively by [39m
[38;5;12m  comparing with "reference implementations" in a pure functional language. [39m
[38;5;12m  Bedrock supports that model, backed by the full expressive power of Coq's [39m
[38;5;12m  usual programming language.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mStructured[0m[38;5;12m: Bedrock is an extensible programming language: any client [39m
[38;5;12m  program may add new control flow constructs by providing their proof rules. [39m
[38;5;12m  For example, adding high-level syntax for your own calling convention or [39m
[38;5;12m  exception handling construct is relatively straightforward and does not [39m
[38;5;12m  require tweaking the core library code.[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mMostly automated[0m[38;5;12m: Tactics automate verification condition generation [39m
[38;5;12m  (in a form inspired by separation logic) and most of the process of [39m
[38;5;12m  discharging those conditions. Many interesting programs can be verified with [39m
[38;5;12m  zero manual proof effort, in stark contrast to most Coq developments.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHACMS[0m[38;5;12m (https://www.darpa.mil/program/high-assurance-cyber-military-systems)[39m
[38;5;12m: High-Assurance Cyber Military Systems (HACMS)[39m
[38;5;12m. Dr. Raymond Richards. Technology for cyber-physical systems,[39m
[38;5;12mfunctionally correct and satisfying appropriate safety and security properties. [39m
[38;5;12mClean-slate, formal methods, semi-automated code synthesis from executable, [39m
[38;5;12mformal specifications. HACMS seeks a synthesizer capable of producing a [39m
[38;5;12mmachine-checkable proof that generated code satisfies functional [39m
[38;5;12mspecs as well as security and safety policies, and development to ensure [39m
[38;5;12mproofs are composable, allowing  components.[39m
[38;5;12m  [39m[38;5;12mmore Darpa "formal" tagged links[39m[38;5;14m[1m (https://www.darpa.mil/tag-list?tt=78)[0m[38;5;12m [39m
[38;5;12m  [39m[38;5;12mverigames-crowdsourced formal verification[39m[38;5;14m[1m (https://www.darpa.mil/news-events/2013-12-04a)[0m[38;5;12m [39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mGenode[0m[38;5;12m (http://genode.org/) : Genode is a novel OS architecture that is [39m
[38;5;12mable to master complexity by applying a strict organizational structure to all[39m
[38;5;12m software components including device drivers, system services, and applications. [39m

[38;2;255;187;0m[4mBooks[0m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mThe Little Prover[0m[38;5;12m (https://mitpress.mit.edu/books/little-prover)[39m
[38;5;12mThe Little Prover introduces inductive proofs as a way to determine facts about[39m
[38;5;12m computer programs.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCertified Programming with Dependent Types[0m[38;5;12m (http://adam.chlipala.net/cpdt/) by[39m
[38;5;12mAdam Chlipala. Textbook about practical engineering with the Coq proof assistant.[39m
[38;5;12mThe focus is on building programs with proofs of correctness, using dependent [39m
[38;5;12mtypes and scripted proof automation.[39m
[38;5;12mLatest draft[39m[38;5;14m[1m (http://adam.chlipala.net/cpdt/cpdt.pdf)[0m[38;5;12m [39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mSoftware Foundations[0m[38;5;12m (https://softwarefoundations.cis.upenn.edu/) by[39m
[38;5;12mBenjamin Pierce and others. The Software Foundations series is a broad [39m
[38;5;12mintroduction to the mathematical underpinnings of reliable software.[39m

[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mVol. 1:[0m[38;5;12m (https://softwarefoundations.cis.upenn.edu/lf-current/index.html)[39m
[38;5;12mread[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/lf-current/toc.html)[0m[38;5;12m [39m
[38;5;12mdownload[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/lf-current/lf.tgz)[0m[38;5;12m [39m
[38;5;12mLogical Foundations, serves as the entry-point to the series. It covers [39m
[38;5;12mfunctional programming, basic concepts of logic, computer-assisted theorem [39m
[38;5;12mproving,and Coq.[39m

[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mVol. 2:[0m[38;5;12m (https://softwarefoundations.cis.upenn.edu/plf-current/index.html)[39m
[38;5;12mread[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/plf-current/toc.html)[0m[38;5;12m [39m
[38;5;12mdownload[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/plf-current/plf.tgz)[0m[38;5;12m [39m
[38;5;12mProgramming Language Foundations, surveys the theory of programming languages, [39m
[38;5;12mincluding operational semantics, Hoare logic, and static type systems.[39m

[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mVol. 3: Verified Functional Algorithms[0m[38;5;12m (https://softwarefoundations.cis.upenn.edu/vfa-current/index.html)[39m
[38;5;12mread[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/vfa-current/index.html)[0m[38;5;12m [39m
[38;5;12mdownload[39m[38;5;14m[1m (https://softwarefoundations.cis.upenn.edu/vfa-current/vfa.tgz)[0m[38;5;12m [39m
[38;5;12mLearn how to specify and verify (prove the correctness of) sorting algorithms, [39m
[38;5;12mbinary search trees, balanced binary search trees, and priority queues.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mHoTT : [39m[38;5;14m[1mHomotopy Type Theory: Univalent Foundations of Mathematics[0m[38;5;12m (https://homotopytypetheory.org/book/)[39m
[38;5;12mpdf[39m[38;5;14m[1m (http://saunders.phil.cmu.edu/book/hott-online.pdfUnivalent)[0m[38;5;12m  [39m
[38;5;12mFoundations of Mathematics is Vladimir Voevodsky’s new program for a [39m
[38;5;12mcomprehensive, computational foundation for mathematics based on the homotopical[39m
[38;5;12minterpretation of type theory. The type theoretic univalence axiom relates [39m
[38;5;12mpropositional equality on the universe with homotopy equivalence of small types. [39m
[38;5;12mThe program is currently being implemented with the help of the automated proof [39m
[38;5;12massistant Coq.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mhttps://math-comp.github.io/mcb/[39m

[38;2;255;187;0m[4mCourses[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mDeepSpec Summer School[0m[38;5;12m (https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw)[39m
[38;5;12m41 Videos about deep specification. Coq videos, examples, tutorials.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mAdam Chlipala Videos:[39m

[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12m2017-12-29[39m[38;5;12m [39m[38;5;12mCCC[39m[38;5;12m [39m[38;5;12mPresentation:[39m[38;5;12m [39m[38;5;14m[1mComing[0m[38;5;14m[1m [0m[38;5;14m[1mSoon[0m[38;5;14m[1m [0m[38;5;14m[1mMachine-Checked[0m[38;5;14m[1m [0m[38;5;14m[1mMathematical[0m[38;5;14m[1m [0m[38;5;14m[1mProofs[0m[38;5;14m[1m [0m[38;5;14m[1min[0m[38;5;14m[1m [0m[38;5;14m[1mEveryday[0m[38;5;14m[1m [0m[38;5;14m[1mSoftware[0m[38;5;14m[1m [0m[38;5;14m[1mand[0m[38;5;14m[1m [0m[38;5;14m[1mHardware[0m[38;5;14m[1m [0m[38;5;14m[1mDevelopment[0m[38;5;12m [39m
[38;5;12m(https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development)[39m

[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mAdam Chlipala Lecture 1, OPLSS 2015[0m[38;5;12m (https://www.youtube.com/watch?v=ORKAy_CHDYM)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mBedrock: A Software Development Ecosystem Inside a Proof Assistant[0m[38;5;12m (https://www.youtube.com/watch?v=BSyrp-iYBMo)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCACM August 2016 - Ur/Web: A Simple Model for Programming the Web[0m[38;5;12m (https://www.youtube.com/watch?v=J3XI6-aZZXk)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mProof engineering Adam Chlipala[0m[38;5;12m (https://www.youtube.com/watch?v=yXLeyANzAC4)[39m
[38;5;12m [39m[38;5;12m [39m[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1m2015 Coq Proof Assistant and Its Applications to Programming-Language Semantics[0m[38;5;12m (https://www.youtube.com/playlist?list=PLt7hcIEdZLAnO7AawDQkHwE7RtwPDOFEc)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mType-Drive Development in Idris - Edwin Brady[0m[38;5;12m (https://www.youtube.com/watch?v=X36ye-1x_HQ)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mBenjamin Pierce - Software Foundations Course[0m[38;5;12m (https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mLearning Automated Theorem Proving[0m[38;5;12m (https://cs.stackexchange.com/questions/820/learning-automated-theorem-proving) : Stackexchange post about learning[39m


[38;2;255;187;0m[4mMore[0m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCurry-Howard[0m[38;5;12m (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) :[39m
[38;5;12mCurry–Howard correspondence refers to the direct relationship between computer[39m
[38;5;12mprograms and mathematical proofs. This is also the idea of "proofs as programs",[39m
[38;5;12mand "propositions (formulas)-as-types".[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHoare logic[0m[38;5;12m (https://en.wikipedia.org/wiki/Hoare_logic)[39m
[38;5;12mHoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system [39m
[38;5;12mwith a set of logical rules for reasoning rigorously about the correctness of [39m
[38;5;12mcomputer programs. [39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mDesigning A Theorem Prover (Paulson, Cambridge, 1990)[0m[38;5;12m (https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-192.pdf)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mRolf Rolles Program Synthesis in Reverse Engineering[0m[38;5;12m (https://www.youtube.com/watch?v=mFjSbxV_1vw)[39m
[38;5;12m...Assume you generate all possible programs...[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mThe Open-Source seL4 Kernel. Military-Grade Security Through Mathematics - SFO17-417[0m[38;5;12m (https://www.youtube.com/watch?v=heSmrHzHcuM)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mDARPA Hack Proof Drones[0m[38;5;12m (https://www.defensetech.org/2014/05/21/darpa-unveils-hack-proof-drone/)[39m
[38;5;12m  Uses SEL4, other RTOS[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mPentagon Wants Unhackable Helicopters[0m[38;5;12m (https://www.engadget.com/2015/03/16/pentagon-wants-unhackable-helicopters/)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHacker-Proof Code Confirmed[0m[38;5;12m (https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/) : [39m
[38;5;12mComputer 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.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCertiKOS enables creation of secure system kernels[0m[38;5;12m (http://www.zdnet.com/article/certikos-a-hacker-proof-os/) [39m[38;5;12mcertikos project[39m[38;5;14m[1m (http://flint.cs.yale.edu/certikos/)[0m[38;5;12m [39m
[38;5;12mComputer system security stinks, because our [39m
[38;5;12msoftware is buggy and untestable in full. Great for cyber criminals, but not [39m
[38;5;12mfor us. So why doesn't someone build a mathematically verified, secure, [39m
[38;5;12mconcurrent kernel that can run on x86 and ARM? A team at Yale has.[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mseL4 Is Free – What Does This Mean For You?[0m[38;5;12m (https://www.youtube.com/watch?v=lRndE7rSXiI)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mFrom L3 to seL4 what have we learnt in 20 years of L4 microkernels?[0m[38;5;12m (https://www.youtube.com/watch?v=RdoaFc5-1Rk)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mseL4 introduction: Capability--based Access Model[0m[38;5;12m (https://www.youtube.com/watch?v=x3P6Y6VO0UI) <- Chinese, translation?[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mseL4 playlist[0m[38;5;12m (https://www.youtube.com/playlist?list=PL8UO9ZG39Nx43YCAKGCtj9Rb6p2_3utdc)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mCreating drones that can't be hacked[0m[38;5;12m (https://www.youtube.com/watch?v=4oONdV5RYp8)[39m
[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mHACMS: Protecting Military Systems from Hackers[0m[38;5;12m (https://www.youtube.com/watch?v=OyqNpn6JpBk)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;14m[1mFormal Methods for Avionics Software Verification pt1[0m[38;5;12m (https://www.youtube.com/watch?v=tRtK4xOK-8o[39m
[38;5;12m)[39m

[48;5;12m[38;5;11m⟡[49m[39m[38;5;12m [39m[38;5;12mTODO: find Heartbleed Example with Agda Showing Proofs[39m
