Category Labs

Formally verify high-risk parts of the Monad implementation, specifically concurrent and parallel execution logic. Build Rocq models of system designs and prove the C++ implementation is equivalent to these models.