This is cool! I work at MakerDao, we are working on formal verification as well. Congrats on YC (again)-look forward to seeing how this project shapes up.