Phase-3 PGD attack on the verified MNIST MLP (planning/archive/robustness.md). Trains the 784→512→512→10 ReLU MLP on the proof-rendered SGD step, then attacks through IREE with the proven mlpInputGrad VJP kernel. The Lipschitz certificate is the product of the three layers' spectral norms — where the bound (and so the cert) goes loose.

Spectral-norm-constrained training of the verified MNIST MLP (planning/archive/robustness_ladder.md, the research lever). Trains the 784→512→512→10 net with projected SGD onto the spectral ball — after every K proof-rendered steps (and once at the end) each weight Wᵢ is rescaled to ‖Wᵢ‖₂ ≤ c (projectSpectral) — then runs the same cert ≤ TRUE ≤ PGD sandwich. Sweeps a few caps c (plus an unconstrained baseline) so the table shows the trade: shrinking c pulls the global L = ∏‖Wᵢ‖₂ down (L ≤ c³), turning the vacuous product certificate non-vacuous — at the cost of clean accuracy. The empirical face of lipschitz_margin_certified_radius (LeanMlir/Proofs/Certificates/LipschitzCert.lean): smaller L ⇒ larger certified radius m/(√2·L). The verified CE gradient stays in the proven kernel; the projection is host-side weight rescaling only.

Generic conv-net PGD attack (planning/archive/robustness_ladder.md). Trains any packed conv net on its proof-rendered SGD step, then attacks through IREE with genKernel — the full proven backward (conv input-VJPs + maxpool select_and_scatter-backs, mirroring the net's <slug>_train_step.mlir) run to dx. Certificate = the conv-aware spectral-norm product (specNormConvTapSum for convs × specNormW for denses; ReLU/maxpool are 1-Lipschitz) — astronomically loose, the depth-cliff. genKernel and net.slug select the architecture (genCnnPgdStep/MNIST-CNN, genCifarPgdStep/CIFAR-CNN).

PGD attack on the verified MNIST CNN (the first conv rung).

PGD attack on the verified CIFAR-10 CNN (the deeper conv rung: 4 conv + 2 pool + 3 dense).

Spectral-norm-constrained training of the verified MNIST CNN (planning/archive/robustness_ladder.md, the gap-shrinking lever applied to the conv net). The CNN sibling of attackPgdSpectralMlp: projected SGD onto the spectral ball — every K proof-rendered steps (and once at the end) projectSpectral caps both the dense ‖Wᵢ‖₂ and the conv tap-sum bound at c — then the cert ≤ TRUE ≤ PGD sandwich (PGD via genKernel, cert = the conv-aware product). Harder than the MLP: it's a k-layer product (L ≤ cᵏ) and the conv tap-sum is a loose bound, so projection over-penalizes the convs — the cert needs a tighter c (and pays more clean accuracy) than the MLP did, and certifies only at smaller radii. The honest "depth + loose conv-norm ⇒ certifying the conv net is harder." Generic over genKernel/net.slug (MNIST-CNN, CIFAR-CNN).

Spectral-norm-constrained training of the verified MNIST CNN.

Spectral-norm-constrained training of the verified CIFAR-10 CNN (7-layer product).

Phase-3 PGD adversarial attack on the verified linear classifier (planning/archive/robustness.md). Trains via the proof-rendered train step, then attacks through the real IREE pipeline: each PGD step's input gradient is computed by the genLinearPgdStep StableHLO kernel (the proven dx = (softmax−onehot)·Wᵀ VJP) on the GPU. Reports clean vs L∞-PGD adversarial accuracy over an eps sweep.

Phase-3 PGD adversarial attack (Chapter 1 linear); see VerifiedNet.attackPgd.

Phase-3 PGD attack on the MLP (Chapter 2); see VerifiedNet.attackPgdMlp.

Phase-3 PGD attack on the CNN (Chapter 3, the conv rung); see VerifiedNet.attackPgdCnn.

Spectral-norm-constrained MLP training study; see VerifiedNet.attackPgdSpectralMlp.

Spectral-norm-constrained CNN training study; see VerifiedNet.attackPgdSpectralCnn.

PGD attack on the CIFAR-10 CNN (the deeper conv rung); see VerifiedNet.attackPgdCifar.

Spectral-norm-constrained CIFAR training study; see VerifiedNet.attackPgdSpectralCifar.