01▲LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean arxiv.org LeanDY marries type-based and trace-based protocol proofs in Lean, finally making symbolic verification wear two hats instead of one.arxivblockchainhashleanprivacyprotocol-verificationsymbolic-verificationtheorem-proving2 pts/jonasl/3 days ago/discuss