The #J-Bob language, a tiny #Lisp for the #formal-methods #tutorial book The Little Prover. This URL also shows how to get a particular file from a #GitHub repo without invoking all their front-end rendering logic.
on 02026-09-17Hillel Wayne on why people don’t use #formal-methods #toread
on 02026-07-30#ebook of the Pascal-F verifier from 01985 by Scott D. Johnson and #John-Nagle. #formal-methods
on 02026-06-14discussion of #formal-methods in the context of #Jane-Street, including #John-Nagle. #toread
on 02026-06-14Yaron Minsky at #Jane-Street, the guy Will has been talking to, wants to adopt #formal-methods now, though previously they haven’t because of the costs. “And those costs are really high! seL4 is a great example of this. It’s a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.” But now they have “agentic coding”, meaning #AI.
on 02026-06-14The #Lean homepage uses “L∃∀N” as the logo but says, “Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code”. #formal-methods
on 02026-06-14You can install #LEAN in a subdirectory with more space by pointing the ELAN_HOME environment variable to it before running elan toolchain install stable or whatever. #documentation #formal-methods
new URL for “a dumb introduction to #Z3”. #formal-methods #toread
on 02026-06-07using #AI #neural-networks to make #SAT solvers work better. #toread #formal-methods
on 02026-03-18#HN discussion of the #AI #LEAN proof of Erdos problem 728, discussing AI and #formal-methods more generally, including the “Lean-language statement of the problem”, which is eight lines of code.
on 02026-01-16#PDF #paper “#ACL2 Support for #Floating-point Computations” #formal-methods
on 02025-11-28“"Flocq" (Floats for Coq) is a formalization of #floating-point arithmetic for the #Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.” #formal-methods
on 02025-11-28#Coq is now #Rocq. #formal-methods
on 02025-11-28"GNATProve" #formal-methods #documentation #toread
on 02025-11-11“Ironclad is a formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software.” GPLv3! #formal-methods include #GNATProve. #operating-systems
on 02025-11-11#PDF #ebook on #formal-methods entitled simply "Formal reasoning", by Herman Geuvers. Propositional logic; predicate logic; discrete mathematics; language theory; automata theory; and modal logic. 131 pp. #toread
on 02025-10-26“a dumb introduction to #Z3”. #formal-methods #toread
on 02025-10-10Discussion of “a dumb introduction to #Z3” #formal-methods #toread
on 02025-10-10#Coq is based on a Calculus of Inductive Constructions which is really a #type-theory. #formal-methods
on 02025-08-06introduction to the #Maude prover, which uses #tree-rewriting. #formal-methods #toread
on 02024-08-25"SMTInterpol" #SMT solver. #formal-methods #SAT
on 02024-06-16#SMT-COMP #PDF #paper about #SMTInterpol, a DPLL(T)/CDCL #SMT solver in Java licensed under LGPLv3. #toread #formal-methods #SAT
on 02024-06-16"CVC5" (Cooperating Validity Checker 5), based on #Minisat, written in C++, and licensed under a 3-clause BSD license, is kind of the top #SMT solver according to the #SMT-COMP results. You can hook it up to #ABC, #CryptoMiniSat, #libpoly, #GMP, #CaDiCal, #symfpu, #CLN (the Class Library for Numbers), and #GLPK. #toread #formal-methods #SAT
on 02024-06-16#SMT-COMP #PDF #paper about the #CVC5 CDCL(T) #SMT solver, the top winner in many categories, licensed under a BSD license. #SAT #formal-methods #toread
on 02024-06-16#SMT-COMP #PDF #paper about #iProver. #toread #formal-methods #SMT #SAT
on 02024-06-16#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16#SMT-COMP winner "Vampire" is under a 3-clause BSD license. #SMT #SAT #formal-methods
on 02024-06-16#SMT-COMP #PDF #paper about #Vampire, a first-order theorem prover. #toread #formal-methods #SMT #SAT
on 02024-06-16#SMT-COMP winner "Yices2" #SMT #SAT #formal-methods
on 02024-06-16#PDF #SMT-COMP paper about the #Yices2 CDCL(T) #SMT solver, which supports three different #SAT solver backends: CaDiCaL, CryptoMiniSat, and Kissat. #formal-methods
on 02024-06-16The "Bitwuzla" #SMT solver, one of the 02023 #SMT-COMP winners, is also under an MIT license. #formal-methods
on 02024-06-16#PDF #paper about the #Bitwuzla #SMT solver at #SMT-COMP, a C++ rewrite of a fork of Boolector. #SAT #toread #formal-methods
on 02024-06-16The "Z3++" #SMT solver, based on #Z3, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16#PDF #paper about the #Z3++ #SMT solver, which is based on #Z3. #SAT #toread #formal-methods
on 02024-06-16#PDF #paper about the #OpenSMT T-DPLL #SMT solver, which is based on MiniSAT. #SAT #toread #formal-methods
on 02024-06-16The "OpenSMT" #SMT (#SAT plus theories) solver, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16#SMT and #SAT competition "SMT-COMP" has many divisions now. #formal-methods
on 02024-06-16"CBMC" is a bounded model checker for #C and C++ programs, part of #CProver. #formal-methods
on 02024-01-30Using #TLA+ #formal-methods for detecting a race condition
on 02023-12-29"Quint" is apparently a veneer over TLA+ with a C-like syntax. #formal-methods
on 02023-07-09“The Limits of Correctness”, Brian Cantwell Smith’s attack on #formal-methods in 01985, basically on the grounds (I’m skimming here) that the properties you can state formally aren’t the ones that will prevent unintentional nuclear war. #PDF #paper
on 02022-05-21using #PRISM, a probabilistic model checker, to model a task queue. #formal-methods
on 02022-05-21#SAL is another of #Shankar’s #formal-methods tools
on 02022-05-21#PVS: #formal-methods in Common Lisp, now free software, by #Shankar
on 02022-05-21the #Metamath proof databases like set.mm are bundled into the 17MB download. #formal-methods
on 02022-05-21“An Introduction to Unification-Based Approaches to Grammar”, Shieber, 1986 (mostly), on #parsing with definite clause grammars and other #formal-methods. #CC by #PDF #ebook #toread 97 pages
on 02021-01-20discussion of #Metamath Zero. #foundations-of-mathematics #formal-methods
on 02021-01-15“Specifying verified x86 software from scratch” Mario Carneiro wants to prove a #Metamath verifier correct with #Metamath. #foundations-of-mathematics #formal-methods
on 02021-01-15Raph #Levien’s #Metamath verifier in 300 lines of Python. #formal-methods #foundations-of-mathematics
on 02021-01-15notes on #formal-methods alternatives for #foundations-of-mathematics, covering #Xena, #Kevin-Buzzard, #LEAN, and #Metamath
on 02021-01-15Verifying popcount, using #formal-methods “more or less out of A Discipline of Programming”; how to invent loop invariants
on 02019-05-20#Z3 #formal-methods #tutorial #toread
on 02019-02-11Neel Krishnaswami (#neelk) explains the difficulties of applying #formal-methods to imperative code. #cs
on 02019-02-01Pamela Zave found a bug in the Chord #DHT protocol using #formal-methods and published a fix. #decentralization
on 02019-02-01Hillel Wayne says #formal-methods aren’t always easier with functional programming, but gives imperative examples that are statically free of aliasing because they don’t use functions.
on 02019-02-01#PDF #paper on how AWS found serious bugs using TLA+ for system design modeling #formal-methods
on 02019-01-22#Adam-Chlipala on how you have to prove that your software doesn’t do undefined things like buffer overflows in order to prove anything at all about it with #formal-methods
on 02019-01-22discussion of #formal-methods with #Hillel-Wayne
on 02019-01-22an #introduction to #formal-methods with #Coq
on 02017-11-25“27 000 Errors in the Tizen Operating System”, #formal-methods for finding bugs in 72 million lines of C++
on 02017-08-0665-page #PDF thesis #paper on #formal-methods #Ethereum #smart-contracts development with #Idris. I think this is the first two-author thesis I’ve seen.
on 02017-07-20Adam Chlipala explains the basis of the Calculus of Inductive Constructions in this chapter of his #ebook on #Coq. #formal-methods
on 02017-07-13#Jean-Yang article on #formal-methods for #security.
on 02017-06-14#Jean-Yang #paper on #formal-methods for #security, ”A language for automatically enforcing #privacy policies” #toread
on 02017-06-14#Jean-Yang #paper on #formal-methods for #security, “Faceted execution of policy-agnostic programs” #toread
on 02017-06-14#Jean-Yang #paper on #formal-methods for #security, “Secure distributed programming with value-dependent types” #toread
on 02017-06-14The original #KANREN homepage: “KANREN is a declarative logic programming system with first-class relations, embedded in a pure functional subset of Scheme. The system has a set-theoretical semantics, true unions, fair scheduling, first-class relations, lexically-scoped logical variables, depth-first and iterative deepening strategies. The system achieves high performance and expressivity without cuts.” #logic-programming #formal-methods
on 02016-11-21Adam Chlipala explains a bit about “library universes” in #Coq. #formal-methods #tutorial #toread
on 02016-08-02Dan Boneh on #Bitcoin and #Ethereum and using #formal-methods for #protocols
on 02016-08-01Safer smart contracts through type-driven development in #Idris: “We show how dependent and polymorphic types can make smart contract development safer. This is demonstrated by using the functional language Idris to describe smart contracts on the #Ethereum platform.” #formal-methods #pdf
on 02016-07-20Ivory is an embedded DSL for Haskell for embedded programming, with a backend that generates C. No heap allocation, but it does do stack allocation, and it doesn’t even have a way to compute a bound on the stack depth. Also has a fixed upper bound on every loop. #formal-methods
on 02016-07-04CBMC is a bounded model checker for #C and C++, using #SAT solvers and SMT solvers to statically check array bounds. Licensed under a 4-clause BSD license. Intended for embedded software. #formal-methods
on 02016-07-04what the #seL4 #security and correctness proofs demonstrate through #formal-methods. Now they don’t trust the compiler and linker.
on 02016-06-29“#Formal-Methods of Software Design” an online course by Eric Hehner: “using mathematics to write error-free programs”.
on 02016-05-31#pdf #tutorial on the HOL-light theorem proving system, which is an embedded DSL for OCaml. #formal-methods #toread
on 02016-05-31A programming language similar to #Idris language in a blockchain with RDF and N3, from the “Intelligent decentralized networks initiative”. “We aim to generalize the concept as much as we find, and give users the ability to implement virtually any P2P network over tau-chain.” #formal-methods
on 02016-05-31of the #Idris tutorials, this “was the most fun to play along with” #sbp #formal-methods
on 02016-05-31#sbp #Idris #pdf #formal-methods
on 02016-05-31#formal-methods #sbp #Idris #formal-methods
on 02016-05-31#formal-methods #sbp #Idris #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #tutorial #pdf #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #tutorial #pdf #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #tutorial #formal-methods
on 02016-05-31#sbp #formal-methods #Idris #tutorial #formal-methods
on 02016-05-31Andrew Appel and Adam Chlipala, among others, are working on this #formal-methods project called DeepSpec.
on 02016-01-11a presentation of a compiler that emits code along with its proof in #Agda, which I guess is a sort of proof assistant? With live Agda code in a page. #formal-methods #compilers
on 02015-11-16Benjamin Pierce’s #introduction to #Coq for #formal-methods, part of an #ebook on the subject. At least the beginning of this chapter seems pretty approachable, much more so than the stuff I’ve seen about ATS and whatnot.
on 02015-08-25The #formal-methods paper on #Coq for programming in #asm, "Coqasm".
on 02015-08-25Using #formalmethods (specifically #Coq and “Crash Hoare Logic”) to specify crash safety for #filesystems.
on 02015-08-23Circus is Z notation for #formal-methods verification of CSP programs.
on 02015-08-16A survey #paper of #parallel #prefix-sum #algorithms, finding that the Kogge-Stone algorithm is more common in #GPGPU code than Blelloch’s, and with handy diagrams so you can see what they’re talking about! Also they apparently wrote a thing to use #formal-methods to verify different implementations.
on 02015-08-15“Practical Foundations for Programming Languages”, an #introduction #ebook to #type-theory for #formal-methods. 2012 to 2014.
on 02015-08-14How to learn #type-theory for #formal-methods.
on 02015-08-14Using #Coq #formalmethods to do a proof of a sort program.
on 02015-08-14using #formal-methods to verify #C #compilers and carry through proofs of your #verifiable-c programs through to the #asm using separation logic. Appel, Leroy, and some others.
on 02015-08-06Wadler explains the #Curry-Howard isomorphism, with a #logic #tutorial into the bargain #formalmethods
on 02015-08-05“Gradual Certified Programming in Coq” #formalmethods
on 02015-08-05