I have not looked at any of it, but would think they'd back it up with some form of math proof for at least some modules, and then applying those algorithms is just like any other C++ or Python code.

People keep saying functional languages are easier to verify but most practical verification tools (model checkers and the like) are built on top of imperative languages.

Ingenuity is a tech demo, so they don't go all out to conserve limited development resource and uses mostly off the shelf hardware and software.