do you know of a good formal specification of the semantics of spreadsheet evaluation?

Topological sort of dependancies is the v0 for spreadsheets, but actual excel supports closed loops a.k.a. circ 's https://basta.substack.com/p/no-sacred-masterpieces which can be used to implement iterative converging algorithms

"We use a circular reference in Excel to do linear regression."

Have a look at the work from Umut Acar on Self Adjusting Computations. https://www.cs.cmu.edu/~rwh/students/acar.pdf The work is cited by the Jane Street guys who implemented Incremental based on those ideas. https://www.janestreet.com/tech-talks/seven-implementations-of-incremental Or the Dependency Graph implemented by the same guys first in Goldman Sachs, then JP Morgan, Bank of America and now Beacon https://www.beacon.io/what-are-dependency-graphs-and-why-are-they-important/