Has anyone ever created a formal specification of the approximate behaviour of some of the components of the NES (in whatever specification language or logical calculus)? In contrast to other consoles like the SNES, the NES being powered by a single clock source would mean this being more easily feasible.

Of course, there are formal specifications for various 6502 core variants, but I am specifically looking for formal models of the added circuitry (the clock circuity, the interrupt system, the bus system, the PPU).

I imagine this would be useful not only for formal reference purposes or emulator writing, but also for symbolic debugging and formal methods of speedrun construction.

I would be glad if someone could provide me with information on attempts or names of people in the scene interested in formal methods.

Of course, there are formal specifications for various 6502 core variants, but I am specifically looking for formal models of the added circuitry (the clock circuity, the interrupt system, the bus system, the PPU).

I imagine this would be useful not only for formal reference purposes or emulator writing, but also for symbolic debugging and formal methods of speedrun construction.

I would be glad if someone could provide me with information on attempts or names of people in the scene interested in formal methods.