F* - Verification system for effectful programs. HOL Light - Computer program to help users prove interesting mathematical theorems completely formally in higher order logic. Verified Software Toolchain - Includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language. SwiftCSP - Constraint satisfaction problem solver written in pure Swift. Logipedia - Project that aims to share formal proofs between several systems. SyGuS competition - Allow solvers for syntax-guided synthesis problems to compete on a large collection of benchmarks. backspace.ai - Fun resource to start playing with formal programming languages. Proof Engineering - Specifying, building, verifying, and maintaining software systems using proof assistants such as Coq, Isabelle/HOL, and HOL4. Runtime Verification - Startup company aimed at using runtime verification-based techniques to improve the safety, reliability, and correctness of software systems. Crucible - Language-agnostic library for performing forward symbolic execution of imperative programs. It provides a collection of data-structures and APIs for expressing programs as control-flow graphs. (Web) (Intro) snarky - OCaml DSL for verifiable computation. FMathL - Formal Mathematical Language. Dafny - Verification-aware programming language. (Docs) Program = Proof - Gives a first introduction to the Curry-Howard correspondence between programs and proofs. (Lobsters) Concrete Semantics - Introduces semantics of programming languages through the medium of a proof assistant.