Verify, but test: extracting property-based tests from F* specifications
summary
Extracts F pre and postconditions into OCaml Boolean predicates via a tiny Meta F tactic and runs them as QCheck tests against production data. Targets an incremental Merkle tree with two invariants Merkle property and left‑to‑right incrementality inside a ~1M LOC Tezos codebase. Builds a readable, reasonably fast prototype OCaml implementation from the model, uses a simple simulation function to map production representation to the model, supports only trivially computable predicates, and finds property testing catches integration issues without full verification.
AI-written summary · about
chapters (10)
- 0:00Industrial verification is hard!
- 3:47Verification spectrum
- 5:11Testing with the initial specification
- 7:28F* Specification Extraction
- 9:11Case study: Incremental Merkle Trees
- 9:43IMT insertion spec
- 10:26Extracted Specification
- 11:04IMT verification
- 11:38Extracted Implementation
- 12:15Testing with the extracted reference
related talks
47mProperty-Based Testing
20mType-level Property Based Testing
51mProperty-Based Testing
42mSurprise yourself with Property Based Testing
01h 24mIntroduction to Property Based Testing
44mHow to specify it! A guide to writing properties of pure functions
36mProperty-Based Testing: Unveiling the Truth on Test Reduction
46mTesting in the world of Functional Programming