run prop pp cmd sign runs the external checker given by the Unix command cmd on the signature sign. The signature is processed and written to a Unix pipe using the formatter pp, and the produced output is fed to the command on its standard output. The return value is Some true in case of a successful check, Some false in the case of a failed check, and None if the external tool cannot conclude. Note that the command cmd should write either "YES", "NO" or "MAYBE" as its first line of (standard) output. The exception Fatal may be raised if cmd exhibits a different behavior. The name prop is used to refer to the checked property when an error message is displayed.