  Causal discovery is a powerful technique for identifying causal relationships
among variables in data. It has been widely used in various applications in
software engineering. Causal discovery extensively involves conditional
independence (CI) tests. Hence, its output quality highly depends on the
performance of CI tests, which can often be unreliable in practice. Moreover,
privacy concerns arise when excessive CI tests are performed.
  Despite the distinct nature between unreliable and excessive CI tests, this
paper identifies a unified and principled approach to addressing both of them.
Generally, CI statements, the outputs of CI tests, adhere to Pearl's axioms,
which are a set of well-established integrity constraints on conditional
independence. Hence, we can either detect erroneous CI statements if they
violate Pearl's axioms or prune excessive CI statements if they are logically
entailed by Pearl's axioms. Holistically, both problems boil down to reasoning
about the consistency of CI statements under Pearl's axioms (referred to as CIR
problem).
  We propose a runtime verification tool called CICheck, designed to harden
causal discovery algorithms from reliability and privacy perspectives. CICheck
employs a sound and decidable encoding scheme that translates CIR into SMT
problems. To solve the CIR problem efficiently, CICheck introduces a four-stage
decision procedure with three lightweight optimizations that actively prove or
refute consistency, and only resort to costly SMT-based reasoning when
necessary. Based on the decision procedure to CIR, CICheck includes two
variants: ED-CICheck and ED-CICheck, which detect erroneous CI tests (to
enhance reliability) and prune excessive CI tests (to enhance privacy),
respectively. [abridged due to length limit]
