In short they are using a scala library called Stainless which is a verification framework which allows for formally proving things about scala programs which use a certain functional subset of scala. This library then plugs into the Z3 Theorem Prover which is one of the most used automated theorem provers/SMT solvers.
To get a better understanding of how it works I’d recommend just taking an hour or two and digging into some material on SAT/SMT solvers online for how they go about proving theorems automatically.