Factorisation of semi-primes n is of number theoretic and cryptographic significance. The Number Field Sieve (NFS) introduced circa 1990, is still the state of the art algorithm, but no rigorous proof that it even halts or generates relationships is known. We propose and analyse an explicitly randomised variant. For each n, we bound the expected time taken to form a congruence of squares modulo n by exp((c+ø(1)) log1/3n loglog2/3 n), with c = 2.77 unconditionally. Assuming the GRH, we prove an upper bound of the same form with c = 3√{[64/9]}, matching the best known heuristic estimate. If n is randomised, we unconditionally bound the harmonic mean of the run time similarly, with c = 3√{[64/9]}.