SAT modulo Symmetries (SMS) is a framework for exhaustive isomorph-free generation of combinatorial objects with prescribed properties. The framework tightly integrates a CDCL SAT solver with a custom dynamic symmetry-breaking algorithm through the IPASIR-Up interface. During solving, partially defined graphs are tested for extendability to canonical fully defined graphs; when extension is impossible, a blocking clause is learned. The framework handles co-NP problems such as non-k-colorability and planarity through additional propagators. SMS generates DRAT proofs, providing an additional layer of confidence in the results. This talk will present the theoretical foundations of SMS, examine applications to extremal combinatorics, and demonstrate the system in action.