I found a solution to our immediate need. There is a Firefox extension called "Copy Plain Text" (
https://addons.mozilla.org/firefox/134/) which cleans the text when you copy it from Firefox (provided you use the Copy as Plain Text item it adds to the right-click menu). So far it works as advertised.
This isn't a solution to the longer term problem of users pasting in junky HTML, but that one is going to be harder to solve.
