Post #4203326

@mario@don.tbully.me @0xabad1dea@infosec.exchange @david_chisnall@infosec.exchange > > the assumption that verifier isn't faulty > that can be proven actually but to remove that assumption and to prove it, you'll need to add some other assumption, maybe about the hardware you'll use to prove the previous assumption, or maybe the model modelling the system on which the theorem prover will run in no way can a theorem prover, escape from its dependence on the assumptions about the system it is running on a normal proof doesn't have any such hidden dependence