Includes completely verified implementations of merge sort and insertion
sort. The synthesis tasks are currently beyond our reach.