Why Checked C when there was Verona?

Let's frame this correctly. Big companies usually offer for free any software that is aimed to bring people into their ecosystem to sell people software that makes hard for people to leave their ecosystem.

Said that, Verona is a new language while checked C is an extension. C has a huge code base out there and people are slowly moving away from C because C is perceived to be unsafe. With checked C people can have a safer C without moving to another language, so it is easier for Microsoft to attract people to their ecosystem with checked C than with Verona.

This is why they have two projects with similar goals.

Because at least Verona is a research language. It is meant for proving concepts, not for writing code for production. I haven't looked into checked c, but one can have multiple research projects in similar directions in order to explore the entire space of possibilities.