Formal verification at scale.

As software gets cheaper to create, more of the work shifts to verifying that programs act as intended. Formal verification provides guarantees about software behavior, but has been held back by slow analysis and expensive specialist labor. We use symbolic execution to build a reusable representation of program behavior, then check specific properties against it under explicit assumptions about the runtime environment.