Formal Verification (Biçimsel Doğrulama)

Formal verification, bir akıllı sözleşmenin belirli özellikleri (güvenlik kuralları) her koşulda sağladığını matematiksel olarak kanıtlama yöntemidir.

Audit'ten farkı: Audit — uzmanlar kodu okur, test eder, açıklar arar (heuristic). Formal verification — matematiksel kanıt ile belirli özelliklerin ihlal edilemeyeceği ispatlınır (deterministic).

Ne kanıtlanabilir: "Bu fonksiyon hiçbir durumda bakiyeyi negatife düşüremez." "Transfer sadece token sahibi tarafından çağrılabilir." "Toplam arz hiçbir zaman X'i aşamaz."

Araçlar: Certora Prover, K Framework, Solidity SMTChecker. Move dili (Aptos, Sui) formal verification için tasarlanmıştır.

Sınırlama: Her özellik formal olarak doğrulanamaz. Maliyetli ve zaman alıcıdır.