Elpi is a higher-order logic programming language derived from $\lambda$Prolog and widely used to extend the Rocq interactive theorem prover. Typical users are familiar with types and functional programming but often lack experience with backtracking.

We introduce a language of signatures to declare that a predicate is operationally deterministic, meaning that calling the predicate does not leave any choice points. The signature language handles higher-order programs and dynamic programs.

We present a static analyzer that verifies these signatures and report its application to the majority of public Elpi code in the Rocq ecosystem.