We present BaB-PoNN, the first formal verification framework for verified robustness of neural networks that use posit arithmetic. BaB-PoNN reasons under the exact posit-8 operational semantics used at inference time, including quire-8 fused accumulation and a single quire-to-posit rounding per affine layer, so every robustness verdict is sound for the deployed implementation. The framework verifies mixed-budget robustness properties in which perturbations are constrained jointly by (i) the number of input coordinates that may change and (ii) the total number of bit flips across those coordinates. We formalize both local robustness, where search is restricted to a data-driven region of interest, and global robustness, where any coordinate may be perturbed within the same hybrid coordinate-bit neighborhood. BaB-PoNN performs an explicit-state search guided by admissible bounds from coordinate swings and per-bit gains, enabling sound pruning while remaining complete: for each input and budget, it either returns a concrete adversarial witness or proves robustness for the specified neighbourhood. Evaluations on posit-8 multilayer perceptron (MLP) and LeNet-5 convolutional neural network (CNN) architectures trained on MNIST show that BaB-PoNN can verify robustness under non-trivial mixed budgets and locate bit-precise adversarial witnesses.