Resolution and CDCL
SAT is NP-complete (The Cook–Levin theorem) yet solvers handle millions of variables.
Formal-Methods
Model Checking, LTL, and Buchi Automata
Exhaustively verifying concurrent systems by turning "always eventually" into an automaton, and the state-explosion wall.
Hoare Logic and Weakest Preconditions
Reasoning about programs as a proof system; loop invariants as the hard part, and why they can't be inferred in general.
Abstract Interpretation and Galois Connections
Sound approximation, made rigorous. The principled answer to the tradeoff Rice's theorem forces on you.
Progress and Preservation
"Well-typed programs don't go wrong", stated as the two lemmas that actually prove it. What a type system does and does not promise.