The main "software" application I'm aware of is a connection to termination checking (whether a program actually finishes). This is in turn connected to automat

The main "software" application I'm aware of is a connection to termination checking (whether a program actually finishes). This is in turn connected to automated complexity analysis, which is a more refined answer about how long a program takes to finish. This is a couple steps removed from all that. Ordinals do show up in the well foundedness check of definitions in ACL2, which is a common lisp interactive proof assistant with applications to software verification. Both of these, while software, are somewhat niche. I'm not aware of a non formal methods / verification software context the ordinals would show up, but I'd love to hear it if so.