Modern software development increasingly relies on multiple vendors and frameworks, often in environments with mutual distrust. Applying formal methods in such settings presents a unique challenge. To address this, we introduce pp-horn, a novel and feasible solver that allows mutually distrusting parties to compute Horn satisfiability (HornSAT) obliviously with minimal leakage. This capability opens the door to a wide range of privacy-preserving formal methods, including oblivious program analysis, invariant generation, relational verification, and logic programming. Motivated by these applications, we design pp-horn as an efficient, plug-and-play secure inference primitive. Our construction leverages secure two-party computation (2PC) via Yao’s garbled circuits (GC) under the semi-honest threat model. Specifically, we design a data-oblivious version of a well-known unit propagation-based algorithm, analyse its asymptotic complexity, and evaluate its empirical performance across various input parameters. As a work in progress, this algorithm represents a foundational first step toward secure multi-party computation (MPC)-based formal methods, and we outline future directions to further optimise and extend this primitive.