# Justicia: A Stochastic SAT Approach to Formally Verify Fairness

arXiv: https://arxiv.org/abs/2009.06516 · HTML: https://mlsanity.com/paper/2009.06516/

## Key facts

- Cited by 25 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Sep 2020.

## Built on by (most cited first, 25 of 25)

- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Adaptive Fairness Improvement Based on Causality Analysis](https://mlsanity.com/paper/2209.07190/) (2022)
- [Algorithmic Fairness Verification with Graphical Models](https://mlsanity.com/paper/2109.09447/) (2021)
- [FairProof : Confidential and Certifiable Fairness for Neural Networks](https://mlsanity.com/paper/2402.12572/) (2024)
- [Monitoring Algorithmic Fairness](https://mlsanity.com/paper/2305.15979/) (2023)
- [How Biased are Your Features?: Computing Fairness Influence Functions with Global Sensitivity Analysis](https://mlsanity.com/paper/2206.00667/) (2022)
- [Verifying Fairness in Quantum Machine Learning](https://mlsanity.com/paper/2207.11173/) (2022)
- [TESTSGD: Interpretable Testing of Neural Networks Against Subtle Group Discrimination](https://mlsanity.com/paper/2208.11321/) (2022)
- [Monitoring Algorithmic Fairness under Partial Observations](https://mlsanity.com/paper/2308.00341/) (2023)
- [A Generic Framework for Conformal Fairness](https://mlsanity.com/paper/2505.16115/) (2025)
- [Active Fourier Auditor for Estimating Distributional Properties of ML Models](https://mlsanity.com/paper/2410.08111/) (2024)
- [Robust ML Auditing using Prior Knowledge](https://mlsanity.com/paper/2505.04796/) (2025)
- [Explainable Global Fairness Verification of Tree-Based Classifiers](https://mlsanity.com/paper/2209.13179/) (2022)
- [Certifying Fairness of Probabilistic Circuits](https://mlsanity.com/paper/2212.02474/) (2022)
- [An Information-Flow Perspective on Algorithmic Fairness](https://mlsanity.com/paper/2312.10128/) (2023)
- [Conformal Prediction: A Theoretical Note and Benchmarking Transductive Node Classification in Graphs](https://mlsanity.com/paper/2409.18332/) (2024)
- [DPER: Dynamic Programming for Exist-Random Stochastic SAT](https://mlsanity.com/paper/2205.09826/) (2022)
- [Sublinear Algorithms for Wasserstein and Total Variation Distances: Applications to Fairness and Privacy Auditing](https://mlsanity.com/paper/2503.07775/) (2025)
- [Language Models That Walk the Talk: A Framework for Formal Fairness Certificates](https://mlsanity.com/paper/2505.12767/) (2025)
- [Monitoring of Static Fairness](https://mlsanity.com/paper/2507.03048/) (2025)
- [Algorithmic Fairness: A Runtime Perspective](https://mlsanity.com/paper/2507.20711/) (2025)
- [The Fair Game: Auditing & Debiasing AI Algorithms Over Time](https://mlsanity.com/paper/2508.06443/) (2025)
- [Energy Shields for Fairness](https://mlsanity.com/paper/2605.24926/) (2026)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)

## Abstract (arXiv)

As a technology ML is oblivious to societal good or bad, and thus, the field of fair machine learning has stepped up to propose multiple mathematical definitions, algorithms, and systems to ensure different notions of fairness in ML applications. Given the multitude of propositions, it has become imperative to formally verify the fairness metrics satisfied by different algorithms on different datasets. In this paper, we propose a stochastic satisfiability (SSAT) framework, Justicia, that formally verifies different fairness measures of supervised learning algorithms with respect to the underlying data distribution. We instantiate Justicia on multiple classification and bias mitigation algorithms, and datasets to verify different fairness metrics, such as disparate impact, statistical parity, and equalized odds. Justicia is scalable, accurate, and operates on non-Boolean and compound sensitive attributes unlike existing distribution-based verifiers, such as FairSquare and VeriFair. Being distribution-based by design, Justicia is more robust than the verifiers, such as AIF360, that operate on specific test samples. We also theoretically bound the finite-sample error of the verified fairness measure.