Formal Methods

Everything and anything that can help automate making software more correct, more robust, etc.

Overview

pressron - Why Writing Correct Software Is Hard

Social Methods

Discipline

• Some thoughts on security after ten years of qmail 1.0 (2007)
• Stamping on event-stream

Complexity

• Algorithmic Complexity 102: user feedback is an instant O(1)
• How Complex Systems Fail

Types

Types in Lisp

• Coalton, a dialect of ML embedded in Common Lisp
• Shen, a Lisp dialect in which you write your own type system with sequent calculus
• Cur, a Racket language with dependent types
• Typed Racket, a Racket language with types
• Hackett, a Racket language like Haskell with macros
• LispNYC presentation on dependent types in 100 lines of Racket by Gershom Bazerman
• Stuck Macros, by Samuel Gélineau
• Rosette, solver-aided programming for Racket

Dependent Types

• Lean
• Cedille, with its "extrinsic" (Curry-style) types as annotations to untyped terms (vs intrinsic / Church style as parts of the term).
• Caledon
• Habit
• Tyrade
• CakeML, and Ramana Kumar's thesis
• Idris, Coq, Agda, F*, ATS, NuPRL, Isabelle, HOL, Epigram, Cayenne...

Logic

Game Theory

• Jules Hedges's compositional game theory bibliography, including The game semantics of game theory.

Protocol Verification

• Noise Explorer

Lightweight formal methods

• fuzzing smart contract compilers

Applied to Blockchain

• ERC777-K
• Formal Verification of OpenZeppelin's ERC20 Token Contract
• Peng Wang's thesis (code, timl)
• Formalization for smart contracts: Scilla-coq (see paper Scilla: a Smart Contract Intermediate-Level LAnguage), TezosCoq, ...

To Sort

• Modularity for Decidability of Deductive Verification with Applications to Distributed Systems, a good approach to proving correctness of complex distributed systems.
• Type System for Resource Bounds with Type-Preserving Compilation and Its Application for Ethereum Smart Contracts can prove bounds on gas usage in some EVM contracts.
• Formal Specification and Verification of Smart Contracts in Azure Blockchain uses model checking to find and fix bugs in simple Solidity contracts.
• Computability Logic
• K Framework,
• Session Types for conversations:
• Parametrized Extensible Effects and Session Types by Oleg Kiselyov,
• Acute and its successor HashCaml by Peter Sewell. Interesting, but they "only" address naming and marshalling, and with a weak security model.
• Cryptographic Protocol Explication and End-Point Projection by Jay McCarthy and Shriram Krishnamurthi (2008), or that cites it, Cryptographic protocol synthesis and verification for multiparty sessions by Karthikeyan Bhargavan, Ricardo Corin, Pierre-malo Deniélou, Cédric Fournet, James J. Leifer (2009). Or things that cite the latter. Conversational Concurrency by Tony Garnock-Jones.
• More Coq for operating systems: Bedrock, CertiKOS
• Formal Method advocacy: What do Formal Methods actually Guarantee?, Formally Verified Software in the Real World,
• Z3 tutorial,
• DeepHOL.
• For complex information propagation during type analysis, ekmett suggests Rete + propagators?