The random K-SAT model gives a model of random Boolean formulas and is perhaps the canonical random constraint satisfaction problem.  The Satisfiability Conjecture posits that the probability of a satisfying assignment undergoes a sharp transition at a critical density of constraints.  Heuristics developed in statistical physics predict the location of the transition as well as much more.  I will survey what is known and predicted and describe recent progress establishing the conjecture for large enough K.  This is joint work with Jian Ding and Allan Sly.