A map $g:\{0,1\}^n\to\{0,1\}^m$ ($m>n$) is a hard proof complexity generator for a proof system $P$ iff for every string $b\in\{0,1\}^m\setminus Rng(g)$, formula $\tau_b(g)$ naturally expressing $b\not\in Rng(g)$ requires superpolynomial size $P$-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan--Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if $A$ is a suitable matrix and $f$ is a $NP\cap CoNP$ function hard-on-average for $P/poly$, then $NW_{f, A}$ is a hard proof complexity generator for Extended Frege.
In this paper, we prove a form of Razborov's conjecture for $AC^0$-Frege. We show that for any symmetric $NP\cap CoNP$ function $f$ that is exponentially hard for depth two $AC^0$ circuits, $NW_{f,A}$ is a hard proof complexity generator for $AC^0$-Frege in a natural setting. As direct applications of this theorem, we show that:

1. For any $f$ with the specified properties, $\tau_b(NW_{f,A})$ based on a random $b$ and a random matrix $A$ with probability $1-o(1)$ is a tautology and requires superpolynomial (or even exponential) $AC^0$-Frege proofs.

2. Certain formalizations of the principle $f_n\not\in(NP\cap CoNP)/poly$ requires superpolynomial $AC^0$-Frege proofs.

These applications relate to two questions that were asked by Krajícek (Cambridge University Press 2019).