AI formal verification को मुख्यधारा में ले आएगा

• Formal verification एक ऐसी विधि है जो गणितीय रूप से यह साबित करती है कि कोड हमेशा specification को पूरा करता है, लेकिन यह लंबे समय तक शोध-केंद्रित सीमित क्षेत्र तक ही सीमित रहा
• seL4 microkernel जैसे कुछ बड़े systems formal verification के साथ विकसित किए गए, लेकिन उच्च जटिलता और लागत के कारण उद्योग में इसका लगभग उपयोग नहीं हुआ
• हाल में LLM-आधारित coding assistant tools ने implementation code के साथ-साथ कई भाषाओं में proof scripts लिखने में भी परिणाम दिखाए हैं, जिससे verification की cost structure को बड़े पैमाने पर बदलने की संभावना बनी है
• अगर AI code generation के साथ correctness proofs को भी automate कर सके, तो development का रुख मानव code review से अधिक भरोसेमंद तरीके की ओर बदल सकता है
• formal verification का automation AI युग में software reliability सुनिश्चित करने की मुख्य तकनीक है, और तकनीकी सीमाओं से अधिक सांस्कृतिक बदलाव इसका mainstream adoption तय करेगा

---

Formal verification की वर्तमान स्थिति और सीमाएँ

• Rocq, Isabelle, Lean, F*, Agda जैसे proof-oriented languages और tools गणितीय रूप से यह साबित करने देते हैं कि code specification को पूरा करता है
  • seL4 operating system kernel, CompCert C compiler, और Project Everest cryptographic protocol stack इसके प्रमुख उदाहरण हैं
• लेकिन उद्योग में formal verification का लगभग उपयोग नहीं होता
  • seL4 के मामले में 8,700 lines of C code के verification के लिए 20 person-years और 200,000 lines of Isabelle code की आवश्यकता पड़ी
  • implementation की हर एक line पर 23 lines of proof और आधे दिन के मानव श्रम की जरूरत होती है
• दुनिया भर में ऐसे proof लिख सकने वाले विशेषज्ञों की संख्या सिर्फ सैकड़ों में मानी जाती है
• आर्थिक रूप से भी अधिकांश systems में bugs से होने वाले नुकसान की तुलना में verification cost अधिक होती है, इसलिए इसकी व्यावहारिकता कम रही

AI कैसे formal verification की अर्थव्यवस्था बदल रहा है

• हाल के LLM-आधारित coding assistants ने implementation code के साथ-साथ proof scripts लिखने में भी प्रदर्शन दिखाया है
  • Nature, Galois, arXiv आदि में ऐसे मामले रिपोर्ट हुए हैं जहाँ LLM ने कई भाषाओं में proofs बनाए
• फिलहाल विशेषज्ञ मार्गदर्शन की जरूरत है, लेकिन कुछ वर्षों में पूर्ण automation संभव होने की उम्मीद है
• verification cost तेजी से घटे तो अधिक software पर formal verification लागू किया जा सकेगा
• साथ ही AI द्वारा generated code के लिए मानव review की जगह formal verification से reliability सुनिश्चित करने की आवश्यकता होगी
  • अगर AI code की correctness खुद साबित कर सके, तो उसे manually written code से भी अधिक पसंद किया जा सकता है

LLM और proof verification की परस्पर पूरकता

• जब LLM proof scripts लिखता है, तब वह गलत सामग्री (hallucination) भी बना सकता है, लेकिन proof checker उसे अस्वीकार कर देता है
  • checker स्वयं verified छोटे codebase से बना होता है, इसलिए गलत proof को पास कराना कठिन होता है
• इसलिए LLM की अनिश्चितता को formal verification की कठोरता संतुलित करती है
• यह संयोजन AI-generated code की reliability सुनिश्चित करने के लिए सुरक्षित automation path की तरह काम करता है

नई चुनौती: specification को सही परिभाषित करना

• automated verification environment में भी specification को सही ढंग से परिभाषित करना मुख्य चुनौती बना रहता है
  • यह सुनिश्चित करना जरूरी है कि proved properties वास्तव में वही हों जो developer चाहता था
• specification लिखने में अब भी विशेषज्ञता और सावधानीपूर्ण सोच की जरूरत है, लेकिन यह manual proof की तुलना में कहीं अधिक सरल और तेज है
• AI natural language और formal language के बीच specification translation में भी मदद कर सकता है
  • हालांकि अर्थ-हानि का जोखिम मौजूद है, लेकिन इसे प्रबंधनीय स्तर का माना जाता है

software development के तरीके में संभावित बदलाव

• developer इच्छित code properties को declarative specification के रूप में लिखेंगे, और AI implementation तथा proof दोनों साथ में generate करेगा
• ऐसी स्थिति में developer को AI-generated code की सीधे समीक्षा करने की जरूरत नहीं होगी, और उसे compiler के machine code की तरह trust-based तरीके से इस्तेमाल किया जा सकेगा
• संक्षेप में, निम्नलिखित तीन बदलावों की संभावना है
  1. formal verification cost में तेज गिरावट
  2. AI-generated code की reliability सुनिश्चित करने के लिए verification demand में वृद्धि
  3. formal verification की precision, LLM की probabilistic प्रकृति की पूरक बनेगी
• यदि ये कारक एक साथ आते हैं, तो formal verification के software engineering की मुख्यधारा की तकनीक बनने की संभावना अधिक है
• आगे चलकर प्रमुख सीमा तकनीक नहीं, बल्कि development culture में बदलाव को अपनाने की गति होगी

[GN⁺]

Hacker News की राय

• मेरा मानना है कि formal verification अपनी असली उपयोगिता उन क्षेत्रों में दिखाता है जहाँ implementation, specification की तुलना में कहीं ज़्यादा जटिल होता है
  जैसे cryptography implementation में bit-level optimization या compiler optimization stages
  लेकिन ज़्यादातर developers (या AI) जो code लिखते हैं, वह पहले से ही high-level languages की वजह से specification के काफ़ी करीब होता है, इसलिए मुझे नहीं लगता कि formal verification का लाभ बहुत बड़ा है
  यह भी स्पष्ट नहीं है कि specification को अलग से लिखना वास्तव में पढ़ने में आसान होगा
  अभी भी कई frameworks और libraries implementation details को abstract कर देते हैं
  formal verification ज़्यादा मज़बूत guarantees दे सकता है, लेकिन ज़्यादातर लोग उस स्तर की guarantee नहीं चाहते, और शायद AI भी यह नई ज़रूरत पैदा नहीं करेगा

• कुछ लोग अनुमान लगाते हैं कि AI formal verification को पूरी तरह automate कर देगा, लेकिन मुझे उस तर्क में समस्या दिखती है
  अगर AI software को अपने-आप prove कर सकता है, तो फिर इंसानों द्वारा लिखे software को verify करने की ज़रूरत ही नहीं बचेगी
  क्योंकि AI खुद ideas सोच सकता है, उन्हें implement कर सकता है, और verification का स्तर तय कर सकता है
  अंततः इंसानों द्वारा की जाने वाली programming या verification गायब हो सकती है
  वास्तव में इंसान proof assistant डिज़ाइन कर सकते हैं, लेकिन उससे बड़े पैमाने के programs verify करना कहीं अधिक कठिन है
  इसलिए अगर ऐसा AI आता है, तो वह खुद नए proof assistants भी बना सकेगा
  बेशक यह कल्पना SF के क्षेत्र के काफ़ी करीब है, और जब हमें यह भी स्पष्ट न हो कि AI किन कामों को आसान या कठिन बनाएगा, तब ऐसी भविष्यवाणियाँ बहुत अर्थपूर्ण नहीं हैं
  संबंधित चर्चा लिंक

  • इंसानों और robots के बीच पहला युद्ध शायद उस क्षण शुरू हो, जब हम “नहीं” कहें और AI कहे, “यह तकनीक मानवता के लिए अच्छी है”
    मुझे लगता है, वही वह turning point होगा जहाँ मानवता पूरी तरह एक नए चरण में प्रवेश करेगी

• coding agents (Claude Code, Codex CLI आदि) से उपयोगी परिणाम पाने के लिए सबसे अहम बात यह है कि उनके लिखे code को run और verify करने का environment अच्छे से तैयार हो
  Python जैसी language, जिसे चलाना आसान हो, सबसे उपयुक्त है, और HTML+JS के लिए Playwright जैसे tools चाहिए
  उसके बाद अगला चरण automated test suite का है, और फिर code formatter, linter, fuzzer जैसे quality tools का
  debugger भी अच्छा है, लेकिन वह interactive होता है, इसलिए agents के लिए उसे संभालना कठिन होता है
  formal verification tools भी इसी spectrum का हिस्सा हैं — क्योंकि आजकल models specialized programming languages को भी अच्छी तरह संभाल लेते हैं
  अगर आपको लगता है कि coding agents ज़्यादा उपयोगी नहीं हैं, तो संभव है कि इसका कारण execution और testing environment की कमी हो

  • strong type system वाली language का उपयोग करना भी बहुत मददगार हो सकता है
    Haskell को उदाहरण लें, तो अगर code compile हो जाए, तो वह लगभग हमेशा सही काम करता है
    अगर यह गुण इंसानों के लिए उपयोगी है, तो LLMs के लिए भी होगा
    खासकर property test LLMs के साथ अच्छी तरह fit बैठता है — क्योंकि कम tests में भी errors के बड़े क्षेत्र को cover किया जा सकता है
    math community में Lean code सुधारने के लिए LLMs के प्रयोग को देखकर लगता है कि अधिक शक्तिशाली type systems का उपयोग करने वाला software development भी पूरी तरह संभव है
  • LLMs के लिए debugging सीखना शायद आसान नहीं होगा
    debugging sequential नहीं होती, और उसमें cause और effect के समय-बिंदु आपस में उलझे रहते हैं
    पहले जब मैंने gdb से multithreaded bug पकड़ते समय ChatGPT का उपयोग करने की कोशिश की, तो वह बार-बार सिर्फ simple print statements जोड़ने की सलाह देता रहा
    अंत में फिर महसूस हुआ कि यह ऐसा क्षेत्र है जहाँ अनुभव और अंतर्ज्ञान की ज़रूरत होती है
  • दिलचस्प बात यह है कि ये tools मानव developers के लिए भी बिल्कुल उतने ही महत्वपूर्ण हैं
    किसी junior engineer से debugger या test runner के बिना काम करने को कहना बेमानी होगा
  • यह काफ़ी मज़ेदार होगा कि model एक semicolon की वजह से “सोचते” हुए बार-बार compile करता रहे
    अंततः शायद और ज़्यादा computing resources की ज़रूरत पड़ेगी
  • मैं Claude Code, Codex और Gemini को multi-agent structure में साथ इस्तेमाल करता हूँ
    Claude implementation करता है, और Codex तथा Gemini review करते हैं
    यह तरीका महँगा है, लेकिन self-bias घटाने और code quality बढ़ाने का सबसे भरोसेमंद तरीका यही रहा है
    static analysis tools अतिरिक्त मदद कर सकते हैं, लेकिन मुझे नहीं लगता कि सिर्फ tools बढ़ा देने से बात बन जाएगी

• अगर verification process automate हो जाए, तो वास्तव में सबसे कठिन हिस्सा specification को सटीक रूप से परिभाषित करना बन जाता है
  proof से ज़्यादा specification लिखना तेज़ और आसान है, लेकिन फिर भी उसमें विशेषज्ञता और सावधानी चाहिए
  पहले formal proof के व्यापक न होने का कारण सिर्फ कठिनाई नहीं था, बल्कि यह भी था कि waterfall approach कम हो गई और agile development मुख्यधारा बन गया
  लंबे specifications लिखने के बजाय, विकास इस दिशा में गया कि user requirements के अनुसार तेज़ी से iterate किया जाए

• लगता है अब OCaml सीखने का समय आ गया है
  कई proof assistants और verification systems OCaml code generate कर सकते हैं, और ADA/Spark पर भी विचार किया जा सकता है
  AI युग में software engineering किसी-न-किसी रूप में बदलेगी, लेकिन हमें आज से और उच्च गुणवत्ता वाला software बनाना होगा
  formal verification इस लक्ष्य में निश्चित रूप से मदद करेगा

• यह अभी अधूरा है, लेकिन मैं अपना experimental project साझा कर रहा हूँ
  code-केंद्रित लेखों की कमी वाली दुनिया में, अगर कोई दिलचस्प hackathon idea ढूँढ रहा हो, तो यह काम आ सकता है
  py-mcmas प्रोजेक्ट लिंक

• LLMs आम तौर पर ऐसी समस्याएँ अच्छी तरह हल करते हैं जिन्हें verify करना आसान हो
  इसलिए मैं problem solving को तीन चरणों में बाँटता हूँ
  1️⃣ पहले success condition program लिखो
  2️⃣ फिर उसी program से मूल समस्या को verify कराओ
  3️⃣ और अंत में मैं खुद जाँच करता हूँ
  यह तरीका मैं पहले से इस्तेमाल करता आया हूँ, लेकिन अब Opus या GPT-5.2 जैसे models इसे unattended mode में भी अच्छी तरह कर लेते हैं
  संबंधित ब्लॉग पोस्ट

  • लेकिन बहुत-सी समस्याओं को verify करना कठिन होता है, और LLMs अक्सर ऊपरी तौर पर सही लेकिन वास्तव में गलत नतीजे बना देते हैं
    जिन क्षेत्रों में verification में बहुत समय लगता है, वहाँ उल्टा इंसानों पर verification का बोझ और बढ़ सकता है

• कोई पूछ सकता है, “verification program को कौन verify करेगा?”
  अगर LLM वही भी लिखे, तो यह अंतहीन turtles all the way down जैसा लग सकता है

  • लेकिन proofs को machine से verify किया जाता है, इसलिए उनके सही होने की जाँच आसान होती है
    कठिन हिस्सा proof बनाना है
    बेशक जटिल propositions में अपवाद हो सकते हैं, लेकिन bugs कम करने में यह बहुत मददगार है

• अगर formal verification mainstream हो भी जाए, तब भी शायद हर कोई Lean या Isabelle इस्तेमाल नहीं करेगा
  बल्कि यह ज़्यादा संभव है कि AI इसे मौजूदा workflow में स्वाभाविक रूप से घुला-मिला दे
  उदाहरण के लिए, CI में property verification, या IDE में “इस module का invariant prove करें” जैसा button
  ज़्यादातर engineers को शायद proof scripts सीधे देखने की भी ज़रूरत नहीं पड़ेगी
  असली कठिनाई यह नहीं है कि LLM proof बनाए, बल्कि यह है कि संगठन specifications और models लिखने में निवेश करें
  अगर AI specifications सुझाना और उन्हें संशोधित करना आसान बना दे, तो verification testing या linter की तरह एक स्वाभाविक refactoring tool बन सकता है

• कुछ लोग शिकायत करते हैं कि GPT‑5.2 “garlic में r कितने हैं” यह भी ठीक से नहीं गिन पाता

  • लेकिन यह driver से वज़न नापने जैसा है
    अगर सच में ज़रूरत हो, तो LLM से Python script लिखवाकर उसे चलाया जा सकता है
  • सच कहूँ तो ऐसी आलोचना उबाऊ लगती है
    बात सही है, लेकिन यह सिर्फ tokenizing implementation detail है और वास्तविक उपयोगिता से लगभग असंबंधित है
    किसी शब्द में कितने अक्षर हैं, यह गिनने के लिए LLM का उपयोग करने की ज़रूरत लगभग कभी नहीं पड़ती