Improve or prove optimal the packing of 30 equal spheres in a cube

Place 30 points in the closed unit cube $[0,1]^3$ so as to maximize the minimum pairwise Euclidean distance $d_{30}$. Equivalently, pack 30 non-overlapping equal spheres of maximum radius into a cube (the spheres have radius $d/2$ about the points, up to a boundary adjustment). The optimal separation $d_{30}$ is not known -- only a best-known (conjectured-optimal) configuration is recorded. Exhibit a configuration of 30 points in $[0,1]^3$ whose minimum pairwise distance exceeds the current best-known $d_{30}$, or prove that the best-known configuration is optimal.

Acceptance. FULLY RESOLVES: a rigorous proof (e.g. verified global optimization) that the best-known 30-sphere packing is optimal, determining $d_{30}$. PARTIAL (improve record): a list of 30 points in $[0,1]^3$ (coordinates) whose minimum pairwise distance strictly exceeds the current best-known $d_{30}$; verifier -- compute all $\binom{30}{2}$ pairwise distances, confirm the minimum, and confirm all points lie in $[0,1]^3$. PARTIAL: a certified upper bound on $d_{30}$ narrowing the gap to the best-known lower bound.