روش‌های صوری؛ از Property تا Assurance Case

پاسخ کوتاه: روش‌های صوری «نرم‌افزار را بی‌باگ» نمی‌کنند. آن‌ها یک ادعای دقیق را دربارهٔ Artifact و Property مشخص، زیر Semantics، Domain، Abstraction و Assumptionهای ثبت‌شده بررسی یا اثبات می‌کنند. خروجی حرفه‌ای یک Formal Assurance Case است که می‌گوید چه چیزی با کدام روش و ابزار، در چه محدوده‌ای، با چه Trusted Base و چه شکاف‌هایی پشتیبانی شده است.

مثلاً «TLC در Config نسخهٔ X، Invariant عدم دوباره‌ثبت‌شدن Event را برای Model محدود به سه Worker و Queue چهارتایی نقض نکرد» ادعایی قابل‌ممیزی است. «همهٔ تراکنش‌های Production امن و درست‌اند» از آن نتیجه نمی‌شود.

مالکیت این مقاله: Formal Assurance Claim

مالکیت محدود این صفحه، ساخت پروندهٔ ادعای صوری از Requirement/Property تا Model/Proof/Result/Implementation gap است. تحلیل استاتیک برای QA عملیات Scanner و Finding را مالک است؛ تست مبتنی بر ویژگی Generator/Shrink/finite sampling را؛ و راهنمای Test Oracle منشأ Expected و Verdict را. این مقاله جای آن‌ها را نمی‌گیرد.

روش صوری یک خانواده است، نه یک Tool

Formal specification، Model checking، Deductive verification/Theorem proving، Abstract interpretation، Symbolic execution، Refinement و Runtime verification هدف و مرز یکسان ندارند. برخی Design model را بررسی می‌کنند، برخی Source را نسبت به Contract، برخی Property را در اجرای جاری. نام روش، Artifact، Property، Semantics و Result vocabulary را دقیق کنید.

روش	پرسش معمول	مرز مهم
Formal specification	رفتار/Property را دقیق نوشته‌ایم؟	خود Specification می‌تواند غلط باشد
Model checking	Model در Domain تعریف‌شده Property را نقض می‌کند؟	Model/config/Bounds و State explosion
Deductive verification	Obligationها از Contract/Logic نتیجه می‌شوند؟	Axiom/Assumption/TCB/termination
Abstract interpretation	در Abstraction، خطای خاص ممکن است؟	False positive و Property family محدود
Runtime verification	Trace مشاهده‌شده Property را نقض کرد؟	فقط اجرای دیده‌شده و کیفیت Instrumentation

Claim را پیش از انتخاب زبان بنویسید

ClaimID / Version / Statement / Subject / Property
Scope / Strength / Audience / DecisionUse / Authority
RequirementSource / HazardOrRisk / Rationale
Formalism / ModelOrCode / Assumptions / Domain
Method / Tool / Result / Evidence / Counterevidence
ImplementationLink / TrustedBase / ResidualGap
ValidityWindow / Expiry / NotClaimed / Correction

«سیستم درست است» Claim نیست. «در Model M، با فرض A و Domain D، هر Posting موفق دقیقاً یک Idempotency key مصرف می‌کند» بهتر است؛ هنوز مشخص نمی‌کند M با Code/Database/PSP واقعی متناظر است.

Subject اثبات را Pin کنید

Subject می‌تواند Requirement، State-machine model، Protocol design، Function، Module، generated code، Source commit، binary یا Hardware model باشد. Repository/commit/file set/build/config/environment/dependency/interface را ثبت کنید. Proof دربارهٔ Design model به Binary دیگری سرایت نمی‌کند.

Property را از شعار کیفیت جدا کنید

• Safety: وضعیت بد مشخص رخ نمی‌دهد؛
• Invariant: Predicate در Stateهای reachable حفظ می‌شود؛
• Liveness: رخداد خوب تحت شرایطی سرانجام رخ می‌دهد؛
• Termination: Computation تعریف‌شده پایان می‌یابد؛
• Functional correctness: با Precondition، Postcondition مشخص برقرار است؛
• Information-flow/Hyperproperty: رابطه‌ای میان چند Execution؛
• Refinement: رفتار سطح پایین با Specification سطح بالاتر سازگار است.

Property باید Formula، Variables، Quantification، Initial/terminal conditions و Strength داشته باشد. «امن»، «قابل‌اعتماد» یا «همیشه کار می‌کند» معمولاً چند Claim حل‌نشده‌اند.

Safety با Safety engineering یکی نیست

Safety property در منطق معمولاً «چیز بد رخ نمی‌دهد» است؛ Safety case مهندسی به Hazard، Environment، severity، fault، mitigation، independence و Evidenceهای چندگانه نیاز دارد. اثبات یک Invariant، کل ایمنی سامانهٔ هوافضا/پزشکی/ریلی را ثابت نمی‌کند.

Requirement ممکن است دقیق اما نامطلوب باشد

Formalization ابهام را آشکار می‌کند، نه اینکه خودکار همهٔ ابهام یا تعارض ارزش‌ها را حذف کند. Requirement source، تفسیر، Stakeholder، risk/hazard، rationale، acceptance و Unknown را نگه دارید. اثبات پیاده‌سازی نسبت به Spec، درستی نیاز انسانی را اثبات نمی‌کند.

Syntax دقیق بدون Semantics دقیق کافی نیست

Language/version/logic/type system، معنای State/step/time/concurrency، integer overflow، floating-point، memory، I/O، exception و undefined behavior را ثبت کنید. یک Formula زیر Integer ریاضی با Machine integer نتیجهٔ یکسان ندارد.

Model باید Environment را هم تعریف کند

ModelID / Version / Digest
Variables / InitialState / Transition / TerminalState
SystemActions / EnvironmentActions / Nondeterminism
Scheduler / Network / Clock / Storage / ExternalService
FaultModel / AttackerCandidate / FairnessAssumption
Abstraction / Omission / Mapping / KnownGap

اگر Network هرگز Packet را Drop/Reorder نکند، Storage هرگز Crash نکند یا PSP همیشه پاسخ دهد، Proof دربارهٔ دنیای دیگری است. ساده‌سازی می‌تواند آگاهانه باشد، اما باید در Claim visible بماند.

Abstraction هم قدرت است هم ریسک

Orderهای بی‌نهایت را شاید به چند State، مبلغ‌ها را به zero/positive، Nodeها را به سه نمونه و Payload را به Token انتزاع کنید. ثبت کنید چه رفتارهایی ادغام/حذف شده‌اند، چرا Property حفظ می‌شود و کدام Counterexample ممکن است Spurious باشد. Abstraction validation یک Evidence مستقل می‌خواهد.

Domain و Bound بخشی از نتیجه‌اند

Constants / Sets / Cardinalities / DataRanges
ProcessCount / QueueBound / RetryBound / TimeBound
MessageLoss / Duplicate / Reorder / Crash / RecoveryBound
SymmetryReduction / Constraint / ExploredStates / Diameter
Completed / Partial / CoverageMeaning / NotExplored

Model checker دربارهٔ Config اجراشده گزارش می‌دهد. «سه Worker و Queue چهار» معادل «هر تعداد Worker و Queue نامحدود» نیست. حتی وقتی Tool تمام Stateهای Model محدود را بررسی می‌کند، تمام Scenarioهای سیستم واقعی بررسی نشده‌اند.

Assumption را Hidden نگه ندارید

AssumptionID / Statement / Type / Source / Owner
WhyNeeded / Justification / Evidence / Confidence
LocalOrGlobal / CallerObligation / EnvironmentCondition
DischargeMethod / RuntimeMonitor / ViolationResponse
EffectiveAt / ExpiresAt / ChangeTrigger

Precondition، invariant کمکی، non-aliasing، initialized input، cryptographic hardness، scheduler fairness، trusted service و correct compiler همگی Assumption candidate هستند. `assume`، `axiom`، `admit` و unchecked external code باید در خروجی دیده شوند.

Proof Obligation واحد حساب است

ObligationID / Context / Antecedent / Consequent
GeneratedBy / DependsOn / Axioms / Assumptions
Status = PROVED | VIOLATED | UNKNOWN | TIMEOUT | SKIPPED
DischargeMethod / Tool / Reviewer / Evidence
Residual / ReopenTrigger / Supersedes

عبارت «Build سبز» تعداد Obligationها، Status یا Skip را نشان نمی‌دهد. یک Timeout/Unknown نباید Pass شود و Proof درصدی بدون Denominator/meaning کافی نیست.

Model Checking چه می‌گوید؟

مستندات رسمی ابزارهای TLA+، TLC را Model checker صریح‌حالت برای Specificationهای اجرایی معرفی می‌کند که Safety و Liveness را بررسی می‌کند. Spec/config/constants/constraints/invariants/properties/tool/options/states/distinct states/diameter/warnings/completion را Pin کنید. Simulation mode یا ناقص‌ماندن Search، exhaustive check نیست.

Counterexample اثبات باگ Production نیست

Trace می‌گوید Model تحت Semantics/Assumptionهای فعلی Property را نقض کرده است. ممکن است Design defect، Spec/Property defect، Environment model نامعتبر یا Abstraction spurious باشد. Initial state، stepها، violation، replay، realizability، mapping به Implementation، triage و disposition را ثبت کنید.

No counterexample مساوی Proof کلی نیست

اگر Search کامل و finite باشد، نبود Counterexample از Property در همان Model/Config پشتیبانی قوی می‌کند. اگر Simulation، constraint، symmetry، fingerprint collision risk، timeout یا resource limit مطرح است، Result محدودتر است. Tool output و warnings را با Interpretation انسانی جایگزین نکنید.

State Explosion را با حذف نامرئی حل نکنید

کاهش Domain، symmetry، compositional reasoning، abstraction، partial-order reduction یا proof ممکن است مناسب باشد؛ هرکدام Claim را تغییر می‌دهد. Bound کوچک را «نمونهٔ نمایندهٔ ریاضی» ننامید مگر دلیل Property-preservation داشته باشید.

Liveness به Fairness/Progress assumption حساس است

بدون فرض Scheduler یا Environment، Action ممکن است برای همیشه اجرا نشود. Weak/strong fairness، stuttering، deadlock، termination و enabledness را دقیق کنید. اضافه‌کردن Fairness برای سبزشدن Property می‌تواند رفتار واقعی Starvation را از Model حذف کند.

Theorem Proving چه چیزی می‌خواهد؟

Definitions، Theorem، Lemma، induction measure، pre/postcondition، frame، invariant، termination و proof dependencyها را نگه دارید. Interactive/automatic بودن و درصد Stepهای machine-checked را روشن کنید. Proof با Axiom یا admitted lemma هنوز Claim مشروط است.

Dafny: صحت نسبت به Specification

Dafny Reference Manual Verification استاتیک Program را نسبت به Specificationهای خود مانند requires/ensures/frame/termination شرح می‌دهد و Toolchain آن از Boogie و Z3 استفاده می‌کند؛ Ghost specification هنگام Compilation حذف می‌شود. Source/project/options، Dafny/Boogie/Z3 versions، assumptions/audit، verification result، generated backend، runtime/FFI و deployment gap را ثبت کنید.

Solver Success را مستقل از Stability ببینید

SMT solver ممکن است با Version، option، resource، trigger یا کوچک‌ترین تغییر Timeout/Unknown شود. چند Seed/resource budget، deterministic build، proof dependency و regression را اجرا کنید. «یک‌بار Verified» به‌تنهایی نگهداری‌پذیری Proof را نشان نمی‌دهد.

SPARK: مرز Proof و Test را مستند کنید

SPARK User’s Guide Flow analysis را از Deductive proof با GNATprove جدا می‌کند. SPARK Reference Manual ترکیب Evidence صوری و تست برای Code خارج Core/Proof، و لزوم Assumptionهای مرز proved/tested را برجسته می‌کند. Mode، Unit scope، contracts، checks، prover، unproved VC، assumptions و boundary tests را Pin کنید.

Trusted Computing Base را فهرست کنید

SpecificationSemantics / Parser / Translator
VCGenerator / ProofKernel / Prover / SMT Solver
Compiler / CodeGenerator / Linker / RuntimeLibrary
FFI / ExternalCode / OS / HardwareModel / CryptoPrimitive
ToolConfig / KnownIssues / IndependentReview / Qualification

TCB هرچه بزرگ‌تر باشد، Claim به اجزای بیشتری اعتماد می‌کند. Machine-checked proof نیز خارج از assumptions، implementation of logic و runtime نیست. «ریاضی» واژهٔ حذف‌کنندهٔ Supply-chain risk نیست.

Refinement پل Model و Implementation است

رابطهٔ abstraction/refinement، state mapping، simulation، representation invariant، generated/manual code و interface را تعریف کنید. اگر TLA+ فقط Design را چک کرده و Code مستقل نوشته شده، Test/Review/traceability لازم است؛ شباهت نام Stateها Proof refinement نیست.

Generated Code انتهای زنجیره نیست

Generator/version/options، target language، compiler flags، libraries، FFI، build digest، platform و runtime effectها را ثبت کنید. Proof Source-to-source ممکن است optimization، undefined behavior، runtime یا deployment config را پوشش ندهد. Binary-level Evidence را جدا بسازید.

Formal Verification و Testing مکمل‌اند

Proof می‌تواند Property مشخص را برای Domain انتزاعی پوشش دهد؛ Test integration، deployment، I/O، dependency، performance، usability، recovery و assumptions واقعی را مشاهده می‌کند. Test ممکن است Counterexample اجرایی بدهد و Mutation/Property tests ضعف Oracle/translation را نشان دهند. یکی را به‌عنوان نسخهٔ «برتر و جامع» دیگری معرفی نکنید.

Validation Specification را مستقل انجام دهید

• Review با Domain expert و affected stakeholder؛
• Example و boundaryهای شناخته‌شده؛
• Simulation/animation قابل‌فهم؛
• Negative property و seeded fault؛
• Alternative formalization/differential model؛
• Traceهای Production-sanitized در صورت مجاز بودن؛
• Independent review و assumption challenge.

این فعالیت‌ها Spec را «اثباتاً صحیح» نمی‌کنند، اما خطر formalizing the wrong thing را کاهش می‌دهند. Reviewer و evidence را ثبت کنید.

Mutation برای Property/Model نیز ممکن است

Transition، guard، invariant، assumption یا refinement mapping را عمداً تغییر دهید و ببینید checker/proof/tests واکنش نشان می‌دهند. Surviving mutant می‌تواند Property ضعیف، unreachable behavior یا equivalent change باشد؛ به فرایند Mutation Testing و triage نیاز دارد، نه Score نمایشی.

Static Analysis را مساوی Formal Proof ندانید

برخی Analyzerها بر Abstract interpretation یا reasoning صوری تکیه دارند، اما Rule scope، soundness/completeness trade-off، unsupported language، build، source-to-sink و suppression مهم‌اند. Zero warning، absence of bug یا کل Propertyهای سطح سیستم را ثابت نمی‌کند.

امنیت به Threat Model و Property مناسب نیاز دارد

Secrecy، authentication، integrity، noninterference، freshness یا protocol correspondence Propertyهای متفاوت‌اند. Attacker capability، cryptographic primitive/assumption، key lifecycle، side channel، implementation و supply chain را مدل کنید. Proof symbolic protocol لزوماً timing/power/cache/entropy/bug پیاده‌سازی را پوشش نمی‌دهد.

Formal Evidence را به Security Control/Evidence pipeline در راهنمای DevSecOps متصل کنید؛ Security testing مجاز و مستقل باقی می‌ماند.

Smart Contract Proof هم Domain-bound است

Invariant Contract بدون Chain/finality/reorg/oracle/bridge/upgrade/wallet/off-chain model کل dApp را پوشش نمی‌دهد. Boundaryهای آن در راهنمای تست Blockchain/dApp آمده است. «Contract verified» را به «دارایی امن است» ترجمه نکنید.

Financial invariant لازم است، کافی نیست

اثبات Debit=Credit می‌تواند Posting نامتوازن را رد کند؛ هنوز Account mapping، source event، currency، fee، authorization، duplicate، settlement یا statement درست را ثابت نمی‌کند. Money/ledger/reconciliation boundary در راهنمای تست نرم‌افزار مالی مستقل است.

Concurrency را با Interleaving واقعی مدل کنید

Atomic step، transaction boundary، weak memory، message reorder، retry، duplicate، crash/recovery و scheduler را تعریف کنید. مدل‌کردن یک عملیات بزرگ به‌صورت Atomic ممکن است دقیقاً Race مورد نظر را حذف کند. Granularity را با implementation mapping بازبینی کنید.

Real-time و Performance معمولاً Claim دیگری‌اند

Logical liveness به deadline، latency percentile یا capacity Production تبدیل نمی‌شود. Clock drift، WCET assumption، scheduler/platform و workload model لازم‌اند. Model timing بدون measurement platform، Performance guarantee نیست.

Tool Version و Option Evidence هستند

Tool / Version / BinaryDigest / Plugin / Solver
OS / Runtime / Hardware / Memory / Workers
Mode / Options / Seed / Timeout / ResourceLimit
KnownIssue / Warning / ExitCode / StartedAt / EndedAt
LogDigest / ReportDigest / Reproducer / ContainerDigest

Defaultها بین نسخه‌ها تغییر می‌کنند. Warning suppressed، simulation mode، incremental cache یا stale result می‌تواند claim را تغییر دهد. Full clean rerun و artifact binding را در Lane مناسب نگه دارید.

Result vocabulary را محدود کنید

PROVED = obligation در Logic/assumptions ثبت‌شده discharged
CHECKED_NO_VIOLATION = search تعریف‌شده نقض پیدا نکرد
VIOLATED = counterexample/proof failure معتبر یافت شد
UNKNOWN = Tool/logic پاسخ قطعی نداد
TIMEOUT / RESOURCE_LIMIT = بررسی کامل نشد
INCONCLUSIVE = Evidence برای Verdict کافی نیست
NOT_RUN / SKIPPED / STALE = Evidence جاری وجود ندارد

`PASS` بدون نوع Result، Subject، Property و Limit خطرناک است. PROVED نیز فقط همان Obligation و dependencies را می‌گوید.

Evidence Pack را Claim-linked بسازید

EvidenceID / ClaimID / SubjectDigest / PropertyID
SpecModelProofCodeRefs / ToolRun / Config / Result
Assumptions / Bounds / TCB / Coverage / Warnings
Counterexample / Review / Test / RefinementEvidence
Collector / Provenance / Integrity / Access / Retention
Limitations / Counterevidence / ValidUntil / Supersedes

Screenshot سبز Tool، Evidence کافی نیست. Source قابل‌بازتولید، log کامل، digest، review و manifest لازم‌اند. Secret/Proprietary model را بی‌دلیل کپی نکنید.

Formal Assurance Case ساختار Argument است

TopClaim
├─ Requirement/Property validity argument
├─ Model/Semantics/Abstraction adequacy argument
├─ Verification result and tool/TCB argument
├─ Assumption discharge/monitor argument
├─ Refinement/implementation correspondence argument
├─ Complementary test/review/runtime evidence
└─ Residual gap, decision, expiry, correction

پرونده باید Counterevidence و شکست‌ها را هم نگه دارد. Assurance strength از تعداد Toolها یا واژهٔ «Proof» نمی‌آید؛ از انسجام Claim-Evidence-Argument و مرزهای صریح می‌آید.

NASA چگونه مرز را نشان می‌دهد؟

مرور رسمی NASA دربارهٔ Formal Methods Model checking را به‌صورت بررسی اینکه Model در Theory انتخاب‌شده Property فرمول‌شده را برآورده می‌کند توضیح می‌دهد و Counterexample را از ویژگی‌های آن می‌داند. این منبع برای Vocabulary است، نه تضمین NASA برای Tool، پروژه یا صنعت دیگر.

Change هر بخش Claim را منقضی می‌کند

• Requirement/Property/interpretation؛
• Semantics/model/abstraction/domain/assumption؛
• Tool/solver/options/known issue؛
• Source/dependency/compiler/runtime/platform؛
• Environment/fault/attacker/workload؛
• Refinement mapping/interface/external code؛
• Counterexample/incident/new evidence.

Impact analysis مشخص کند کدام Obligation/Proof/Run/Test/Decision باید Reopen شود. Badge دائمی «Formally verified» بدون Artifact/version/validity window قابل‌ممیزی نیست.

Correction تاریخ Proof را پاک نمی‌کند

اگر Property اشتباه، Model ناقص، Assumption نامعتبر، Tool bug یا mapping غلط کشف شد، CorrectionID، old/new claim، affected release/consumer، reason، new evidence، decision و confirmation بسازید. گزارش قبلی را Silent edit نکنید.

آزمایش قطعی: پنج چراغ سبز ناکافی

یک Validator مستقل و بدون Dependency با Node.js ۲۴.۱۸.۰ روی Fixture کاملاً ساختگی اجرا شد. Checker سطحی فقط Formal spec، Model-check pass، Theorem-prover pass، Static-analysis clean و All-tests-passed را دید و به‌اشتباه نتیجه داد:

SUPERFICIAL=MATHEMATICALLY_CORRECT_SECURE_AND_BUG_FREE

پس از اصلاح یک Assert اولیه از ۲۸۰ به شمار واقعی Deduplicated، ممیز با اجرای پاک ۲۷۸ کنترل یکتا را در ۲۸ گروه Identity، Claim، Target، Requirement، Formalism، Property، Model، Domain، Assumption، Obligation، Method، Tool، Execution، Result، Counterexample، Proof، TCB، Refinement، Implementation، Validation، Evidence، Change، Finding، Decision، Lifecycle، Security، Safety و Limits بررسی کرد. هیچ‌کدام در Fixture سطحی نبود:

CONTROL_COUNT=278
AUDIT=HOLD-278
INDEPENDENT_TARGET=real-system-or-production:false:PASS

قاعدهٔ مستقل تأیید کرد هیچ System یا Production واقعی بررسی نشده است. پس از پرکردن همهٔ فیلدهای ساختاری با مقدار ساختگی و مرزهای no all-scenarios/no bug-free/no requirement-validity/no implementation-correctness/no security/no safety/no reliability/no compliance/no real-world-adequacy proof، نتیجه شد:

CORRECTED=READY_FOR_FORMAL_ASSURANCE_REVIEW-0
BOUNDARY=structure-only; no all-scenarios coverage, bug freedom,
requirement validity, implementation correctness, security,
safety, reliability, compliance, or real-world adequacy proven

چرا صفر Finding هنوز Proof نیست؟

Validator فقط Completeness Record را می‌سنجد. Formula، semantics، model adequacy، solver soundness، reviewer reasoning یا implementation mapping ممکن است غلط باشند. `READY_FOR_FORMAL_ASSURANCE_REVIEW` نتیجهٔ صوری Property نیست.

آزمایشگاه فارسی کاملاً آفلاین

یک State machine خیالی برای Checkout محلی بسازید: Order، PaymentAttempt، PSP Stub، Callback، Ledger، Reconciliation و Notification. Property محدود: «برای هر EventID ساختگی accepted، بیش از یک Posting effect ساخته نمی‌شود» و «State version کاهش نمی‌یابد». Model فقط دو Order، سه Event، Queue چهارتایی و حداکثر دو Retry دارد.

عمداً Duplicate، late، reordered، timeout-before/after-fake-commit و stale-version را مدل کنید. یک Bug در dedupe transition Counterexample می‌دهد؛ سپس Fix را Check کنید. بعد Mapping ناقص به JavaScript stub را تزریق کنید تا نشان دهد Model pass بدون refinement/test، Implementation را پوشش نمی‌دهد.

LabBoundary = {
  network: false,
  production: false,
  realSystemOrOrganization: false,
  realPersonOrPayment: false,
  realSafetyOrSecurityClaim: false,
  legalOrComplianceOpinion: false,
  purpose: "validate formal-assurance record mechanics only"
}

IRR کاملاً خیالی و تومان فقط Label نمایشی است. ارقام فارسی/عربی/لاتین، ی/ی، ک/ک، ZWNJ، RTL/LTR/Bidi، UTC/Asia-Tehran و Jalali صرفاً نمایشی پوشش داده می‌شوند. هیچ Bank/PSP/account/person/PAN/CVV2/OTP/cookie/token/credential/log/screenshot یا قانون/حسابداری واقعی وجود ندارد.

تمرین پنج‌مرحله‌ای Assurance Case

1. Claim/Property/Not-claimed و Subject را Pin کنید.
2. Model/semantics/domain/assumptions را با Bounds صریح بنویسید.
3. Counterexample خراب را Replay، Triage و Fix کنید.
4. Result/TCB/refinement/test evidence را به Argument وصل کنید.
5. یک Assumption را نقض و Expiry/Correction/affected decision را تمرین کنید.

Anti-patternهایی که باید رد شوند

• «Formal است، پس بدون ابهام و درست است»؛
• «Model checker همهٔ Scenarioها را بررسی کرد»؛
• «Counterexample یعنی باگ قطعی Production»؛
• «No counterexample یعنی سیستم بی‌باگ است»؛
• «Bound کوچک نمایندهٔ ریاضی همهٔ اندازه‌هاست»؛
• «Fairness assumption فقط سرعت Search را بهتر می‌کند»؛
• «Theorem proved شد، پس Requirement معتبر است»؛
• «SMT success یعنی هیچ Axiom/Assumption نداریم»؛
• «Machine checked یعنی TCB صفر است»؛
• «Design model pass یعنی Source/Binary درست است»؛
• «Generated code نیاز به Test ندارد»؛
• «Zero static warning یعنی Proof»؛
• «Formal security proof یعنی هیچ Side channel نیست»؛
• «Ledger invariant یعنی تراکنش مالی درست است»؛
• «Liveness یعنی Deadline رعایت می‌شود»؛
• «Proof جای Test/User research/Monitoring را می‌گیرد»؛
• «Tool badge برای همیشه معتبر است»؛
• «Timeout را می‌توان به‌عنوان Pass نگه داشت»؛
• «تعداد Proof obligation معیار کیفیت محصول است»؛
• «فرم کامل یعنی امنیت، ایمنی و صحت ثابت شده است».

چک‌لیست Owner پیش از ادعای صوری

• Claim/Subject/Property/Scope/Strength/Not-claimed نسخه‌دارند.
• Requirement source/interpretation/risk/authority روشن است.
• Formalism/logic/semantics/type/time/concurrency مشخص‌اند.
• Model initial/transition/environment/fault/omission ثبت شده‌اند.
• Abstraction mapping و validation evidence وجود دارد.
• Domain/bounds/constraints/explored state کامل گزارش شده‌اند.
• Assumption/axiom/admit/precondition/expiry visible است.
• Proof obligationها Denominator و Status دقیق دارند.
• Method family و soundness/completeness limit روشن است.
• Tool/solver/version/digest/options/resource/warnings Pin شده‌اند.
• Counterexample با realizability/mapping/disposition Triage شده است.
• Proof theorem/lemma/axiom/trusted/unchecked step دارد.
• TCB شامل translator/compiler/runtime/external code است.
• Refinement از Model تا Code/Interface شواهد دارد.
• Generated/manual code و deployment gap ثبت‌اند.
• Test/review/simulation/runtime evidence مکمل‌اند.
• Security/safety claims Threat/Hazard جدا دارند.
• Result از PROVED/CHECKED/UNKNOWN/TIMEOUT دقیق است.
• Evidence claim-linked/provenance/integrity/retention دارد.
• Decision owner، condition، residual risk و dissent ثبت‌اند.
• Change impact و clean recheck تعریف شده‌اند.
• Correction به Claim/release/consumer متاثر رسیده است.
• هیچ All-scenarios/bug-free/security/safety guarantee داده نشده است.

Pilot سی‌روزهٔ Formal Assurance

هفتهٔ اول: یک Risk کوچک همزمانی را به Claim/Property/Not-claimed تبدیل کنید. هفتهٔ دوم: Model و Domain محدود بسازید و یک Counterexample عمدی بیابید. هفتهٔ سوم: Assumption/TCB/refinement و Testهای مکمل را اضافه کنید. هفتهٔ چهارم: Change، clean recheck، Decision و Correction را در CI تمرین کنید.

شاخص Pilot تعداد Proof یا State نیست. Claim مبهم، Property بدون Requirement، Model بی-environment، Bound پنهان، Assumption discharge‌نشده، Timeout سبز، Tool بی‌نسخه، TCB گمشده، Model-Code gap، Counterexample بسته‌نشده و Badge منقضی را بسنجید. این سنجه برای رتبه‌بندی افراد نیست.

منابع چگونه استفاده شده‌اند؟

NASA برای Vocabulary مدل/Property/Model checking/counterexample؛ منابع رسمی TLA+ برای مرز Spec/TLC/TLAPS و finite explicit-state checking؛ Dafny برای Verification نسبت به Contract و زنجیرهٔ Boogie/Z3/Compilation؛ و SPARK برای جداسازی Flow/Proof، Assumption و ترکیب Evidence اثبات/تست استفاده شدند. هیچ منبعی ادعای بی‌باگ/امن/ایمن دربارهٔ پروژهٔ این مقاله نمی‌دهد.

جمع‌بندی

قدرت روش صوری در محدودکردن دقیق ادعاست: Property مشخص، Model و Semantics معلوم، Domain و Assumption آشکار، Tool/Proof قابل‌بازتولید و پل روشن تا Implementation. هرجا این زنجیره قطع شود، Assurance Case باید Gap را نشان دهد. Proof خوب جای واقعیت را نمی‌گیرد؛ توضیح می‌دهد تحت چه قرارداد منطقی چه چیزی می‌دانیم و هنوز چه چیزی را نمی‌دانیم.

سوالات متداول

آیا روش‌های صوری همهٔ باگ‌ها را حذف می‌کنند؟

خیر. یک روش صوری Property مشخص را دربارهٔ Model/Code مشخص، زیر semantics و assumptions مشخص بررسی می‌کند. Requirement غلط، Property ناقص، Model-Code gap، Tool/TCB، dependency، محیط و رفتار خارج Scope باقی می‌مانند.

تفاوت Model Checking و Theorem Proving چیست؟

Model checking معمولاً Stateهای Model/Config محدود را خودکار جست‌وجو و Counterexample تولید می‌کند؛ Theorem proving با Logic، Lemma و استنتاج Obligationها را discharge می‌کند و می‌تواند Parametric باشد، اما به Proof/Assumption/TCB دقیق نیاز دارد. انتخاب به Property و Claim بستگی دارد.

اگر TLC هیچ Counterexample نداد، سیستم درست است؟

فقط می‌توان دربارهٔ Property، Model، Config، bounds و completion همان Run ادعا کرد. Abstraction، environment، constraint، fairness assumption و ارتباط Model با Implementation باید جدا ارزیابی شوند.

آیا کد Verified هنوز به تست نیاز دارد؟

معمولاً بله. تست می‌تواند interface، dependency، generated binary، deployment، performance، UX، recovery و فرض‌های runtime را پوشش دهد. نوع تست را از Gap پرونده انتخاب کنید، نه برای تکرار بی‌هدف Proof.

QA چه Artifactی از Formal Methods بخواهد؟

Formal Assurance Case شامل Claim/Property، Subject digest، model/spec/proof، semantics/domain/bounds/assumptions، tool/solver/options/run، result/counterexample، TCB، refinement/implementation link، complementary tests، residual gaps، decision، expiry و correction.