The exception was [1], a Lean-based text heavily inspired by Concrete Semantics [2], a cornerstone of Isabelle literature. The latter is, in essence, Winskel's classic semantics book [3], a standard textbook in programming language theory, with all proofs mechanically checked.

More broadly, I'm wondering whether dependent types are the right abstraction or too powerful and heavy for humans to review and make sure specifications are aligned with intent. I've been working on automation for this for more than a year, and I've found refinement types sufficient and much easier to review.

[1] https://github.com/lean-forward/logical_verification_2025

[2] http://concrete-semantics.org

[3] https://direct.mit.edu/books/monograph/4338/The-Formal-Seman...