anyhow, not going to far, I have an observation: 1. sometimes a proof is too trivial, the effort of making one seems not justified. 2. a complex proof that is worth making to make a library "proven correct" are the cool ones. I have seen rb tree implementation, what else interested you? 3. actual system behaviour seems better modelled by linear-time temporal logic or model checking. that seems not what dependent type does, is it?