Cameleer: a Deductive Verification Tool for OCaml
summary
Cameleer takes OCaml source annotated with Gospel specs, translates the AST to Why3 and emits VCs solved by SMTs (demo uses Alt-Ergo); it targets core OCaml (no objects, limited GADTs/polymorphic variants, restricted higher-order and mutable-recursive structures). The tool verifies many case studies—most proofs fully automatic, union‑find is fully discharged, a small arithmetic‑to‑stack compiler is verified—and offers both an interactive Why3 IDE and a batch mode for automated checking.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:55Deductive verification
- 2:38What we need
- 3:46The Cameleer Project
- 4:39Gospel
- 5:47Camel Attributes
- 7:03Outline
- 7:33How Cameleer works
- 10:05Demonstration
- 18:07Constraints
- 19:39Recursive Functions
- 20:35Cycles
- 21:11Ghost Functions
- 22:34Always Lists
- 23:29Module Language
- 24:11Functors
- 25:06Conclusion
- 26:08Future plans