They can implement an algorithm. It is not the same as writing tons of pages of a machine code level automated theorem prover. Except someone wrote a library f

They can implement an algorithm. It is not the same as writing tons of pages of a machine code level automated theorem prover. Except someone wrote a library for timing proofs (including cache and memory) in Isabelle/HOL already, but it has to be combined with the recompile prover from SeL4 project. That would take some time and work.