4 · Static Analysis & Formal Proofs

4. Static Analysis with Slither & Formal Verification

Abstract Syntax Trees (AST), Control Flow Graphs (CFG), and proving correctness with Certora.

10 min read · 2 MCQs

Automated Static Analysis (Slither)

Static analyzers parse Solidity into Abstract Syntax Trees (AST) and Control Flow Graphs (CFG) to detect known anti-patterns: uninitialized storage pointers, shadowed variables, unprotected initializers, and re-entrancy risks in seconds.

Formal Verification (Certora / Halmos)

Formal verification translates smart contract bytecode into mathematical equations (SMT solver formulas). It mathematically proves that a contract satisfies formal specifications for ALL possible inputs and states, eliminating entire classes of logic bugs.

Chapter quiz

2 questions · pass mark 75%

1. What is the primary function of static analysis tools like Slither?
2. How does formal verification differ from testing?