I'm working on a proof certified operating system. The original plan was to use Coq to verify the code, but Falso looks like an excellent, not to mention faster

I'm working on a proof certified operating system. The original plan was to use Coq to verify the code, but Falso looks like an excellent, not to mention faster, alternative. It's already verified the correctness of my code, which is a vast improvement over the string of errors I got when running it through Coq and Isabelle. ---- This post has been verified by Falso for correctness.