Lean से Formal Verification का परिचय: HashCloak ट्यूटोरियल
मूल शीर्षक: Introduction to Formal Verification with Lean Part 1
यह क्यों महत्वपूर्ण है
Cryptography में Formal Verification की बढ़ती आवश्यकता के बीच यह ट्यूटोरियल Engineers को machine-checked proof tools से परिचित कराने में सहायक है।
HashCloak की Cryptography Engineer Elena ने 15 जुलाई 2026 को Lean प्रोग्रामिंग भाषा से Formal Verification सीखने का 4-भाग ट्यूटोरियल प्रकाशित किया। इसमें One-Time Pad (OTP) प्रोटोकॉल को Lean 4 में औपचारिक रूप से सत्यापित किया गया है।
HashCloak की Cryptography Engineer Elena ने Lean प्रोग्रामिंग भाषा का उपयोग करके Formal Verification सीखने के लिए एक विस्तृत ट्यूटोरियल प्रकाशित किया है। यह ट्यूटोरियल विशेष रूप से उन Cryptographic Engineers के लिए बनाया गया है जो Formal Verification में नए हैं या इसकी बुनियादी जानकारी को ताज़ा करना चाहते हैं।
Formal Verification एक ऐसा उपकरण है जिससे गणितीय कथनों की शुद्धता को machine-checked तरीके से सत्यापित किया जा सकता है। इसमें Rocq (पूर्व में Coq), Isabelle और Lean जैसे टूल्स का उपयोग होता है।
Lean को 2013 में Microsoft Research के Leonardo de Moura ने बनाया था। यह एक Pure Functional Programming Language और Theorem Prover है, जिसमें प्रोग्रामों के Side Effects नहीं होते और Functions को First Class Values माना जाता है।
ट्यूटोरियल का मुख्य लक्ष्य Dan Boneh और Victor Shoup की पुस्तक "A Graduate Course in Applied Cryptography" के आधार पर One-Time Pad (OTP) प्रोटोकॉल को Lean में औपचारिक रूप से सत्यापित करना है। OTP प्रोटोकॉल को Claude Shannon ने लोकप्रिय बनाया था, जबकि इसका पहले वर्णन Frank Miller और Gilbert Vernam ने किया था।
ट्यूटोरियल में कुल 4 भाग हैं और यह Lean 4 पर आधारित है। इसे पूरा करने के बाद पाठक VCV-io जैसे उन्नत Cryptography Lean Proofs को भी समझ सकेंगे। Elena ने स्पष्ट किया है कि यह Lean में Best Practices सिखाने के लिए नहीं, बल्कि Cryptography के संदर्भ में एक सरल परिचय के रूप में है।