PICK helps you build an LTL formula from a natural-language description by iteratively refining it with example traces.

You start by describing the temporal behavior your property should capture.

PICK sends that description to an LLM of your choice to surface several plausible interpretations as candidate LTL formulas.

It then shows example traces, and your votes (should this trace satisfy the property?) narrow down which formula best matches your intent.

PICK is research software. You may encounter rough edges or unexpected behavior. We appreciate patience, bug reports, and especially concrete cases where the tool either works particularly well or misses the mark—these directly inform our research.