En deltaker ved Recurse Center forsøkte å formalisere læreboken Abstract Algebra av Dummit og Foote i beviskontrollsystemet Rocq, og støtte da på en reell feil i boken. Arbeidet illustrerer hvor nyttig formell verifisering kan være for å avdekke subtile matematiske feil.