The problem of synthesizing specifications of undefined procedures has a broad range of applications. However, the usefulness of the generated specifications depends on their quality. In this talk, I will present our work on finding correct and maximal specifications using an approach called infer-check-weaken. This approach first infers a correct specification through a logical synthesis technique. A maximality check follows to determine whether the specification is the weakest. If not, the specification is weakened. We observe that our approach is effective across a range of benchmarks, including those with arrays.