Design by Provable Contracts

Overview

AI, Data Science & Cloud Certificates from Google, IBM & Meta — 50% Off

One plan covers every Professional Certificate on Coursera. 50% off Coursera Plus Annual for 10 days only — price increases June 17.

Unlock All Certificates

e.g. This is primarily aimed at first- and second-year undergraduates interested in engineering or science, along with high school students and professionals with an interest in programming.Design by Provable Contracts teaches you how to move from "the tests pass" to "the math says it cannot break." Across five modules, you'll climb a five-rung provability ladder — from lint and types, through property-based and bounded-model checking, to dependent-typed proofs in Lean 4 — applied to a single running example: the softmax function used in modern machine learning. By the end, you will be able to: (1) read a peer-reviewed paper and translate its preconditions, postconditions, and invariants into a YAML contract; (2) choose the right verification rung for a given cost-vs-confidence trade-off, using lint, types, proptest, and Kani in Rust; and (3) build a complete pipeline from paper to YAML to Lean theorem, producing a machine-checked guarantee that holds for every input of every length. The course is hands-on and tool-first: Rust for the lower rungs, Lean 4 for the top rung, and YAML as the connective tissue between math and code. You will leave with a reusable mental model and a working capstone you can apply to any safety-critical numerical kernel.

Syllabus

The DBC Pillar — Caller/Callee Contracts

Master Hoare triples and the contract foundations of Design by Contract. Learn how {P} S {Q} formalizes preconditions, postconditions, and the caller/callee responsibility split through Eiffel's require/ensure idiom and its Rust port via Prusti and Creusot.

The Type-System Pillar — Contracts via the Type-Checker

Shift contracts from runtime checks into the type system. Learn parse-don't-validate, the newtype pattern as a zero-cost contract, and typestate to encode state machines directly in types so invalid states cannot be represented.

The YAML Bridge — Papers, Math, Contracts in Code

Use a YAML contract as the machine-readable, human-auditable bridge between research papers and verified Rust kernels. Learn the 19-property obligation taxonomy, Popperian falsification testing, and how pv aggregates L1 to L5 status into one audit artifact.

Climbing the Provability Ladder — L1 to L5

Walk the proof ladder on softmax: L1 lint, L2 types, L3 proptest, L4 Kani bounded model checking, and L5 Lean theorems. Learn to pick the rung that matches the cost of being wrong.

Capstone — softmax Across All Five Levels

End-to-end capstone: take softmax from a peer-reviewed paper, through a YAML contract, to a Lean 4 theorem holding for every finite vector of every length. Every cell of the Lesson 1.1 tooling map gets demonstrated.