In teletraffic engineering, M/G/1 queues are pivotal for optimizing network performance and operational efficiency. Closed formulas like the mean-value Pollaczek-Khinchin (MV-PK) are highly valued by practitioners due to their simplicity, facilitating rapid and flexible system analyses. This formula aids in verifying the reliability of complex simulations concerning M/G/1 models, especially when applicable. The challenge intensifies when dimensioning M/G/1 systems with heavy-tailed service time distributions. Simulation of such queues becomes notably arduous, necessitating increased number of samples and longer simulation durations. Moreover, verification becomes more intricate as the MV-PK formula cannot be straightforwardly applied in such cases. This paper extends the MV-PK formula to heavy tailed service distributions with infinite/infinitesimal moments using Nonstandard Analysis. Additionally, it shows how recently introduced Bounded Algorithmic Numbers (BANs) enables numerical verification of the extended PK formula via discrete-event simulations of the M/G/1 queue, even when predicted delay values are infinite. The implemented approach tends to converge fast and exhibits remarkable numerical robustness. It adheres to the principle of “write once, run multiple times", as the same source code for queue simulation handles both finite and infinite variance cases.