An approach to software development with the aim to product programs guaranteed to be correct with respect to their Specification.
Process
- Encode specification into logical formula
- Use SMT Solver or Synthesis Algorithm (Often enhanced by Heuristic) + Oracle