@mario @0xabad1dea something something turtles all the way down?
@mario @0xabad1dea Assuming that the verification mechanism is perfect.
@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it.
There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer.
Jul 29, 2026, 11:01 AM@mario @0xabad1dea @shelldozer right, that's not a bug in software
so, you can say the following isn't true for metarocq
> Theorem provers aren't magic, and have bugs just like all other programs.
but having the probability of hardware issues still makes the following true
> Theorem provers aren't magic
Jul 29, 2026, 11:04 AM@mario @0xabad1dea @shelldozer not to say, they aren't magic, like i love theorem provers, and they are in a way very magical pieces of software humans have come up with
all this means is they shouldn't become the single source of truth
Jul 29, 2026, 11:17 AM@mario @0xabad1dea @calx @shelldozer Even with a flawless theorem prover, it is possible that what was proved isn't what you think it is because you made a mistake when formalising the theorem.
Jul 29, 2026, 5:15 PM@mario @0xabad1dea @calx @shelldozer @mansr if the person in question is formalizing a theorem prover, then that's definitely in the scope of problems.
Also you run into some gödel-esque problems when trying to fully prove the consistency of a theorem prover, within the theorem prover itself, so there are probably _some_ limits
Jul 29, 2026, 11:19 AM@mario @0xabad1dea @shelldozer ooo, interesting
tho, i'll have to read about them and metarocq before i can comment
Jul 31, 2026, 7:30 PMJul 29, 2026, 10:56 AM@mario @0xabad1dea the hardware can be faulty too, tho. no? and we can have a bit flip error, tho that can be avoided by checking multiple times
edit: it was already mentioned, my bad
Jul 29, 2026, 1:28 PMVerification is only as good as the models and the properties you verify.
My favourite example of this was a verified Arm core, which had dataflow proofs of all of its TrustZone implementation. This was then laid out for the back end in such a way that the wire that carried the TrustZone state went very close to another wire. Running the right sequence of instructions would induce a current and toggle from NS to S state, allowing unprivileged instructions to jump to secure mode (the layout was done as a research demonstration, not something in real production).
So even the security properties that were formally verified on the RTL were not actually present in the physical silicon.
Jul 29, 2026, 1:53 PMOr, as I like to put it:
Formal verification is a technique for ensuring that your bugs are present in your specification.
But that wasn't actually quite the issue here, the verification was against an abstract machine and the concrete machine did not quite reflect the abstract machine.
Jul 29, 2026, 1:55 PM@mario Nope, they were treated as axioms.
Jul 29, 2026, 2:10 PM@mario There is some really exciting work to try to prove equivalence between the various layers of lowering from RTL to silicon, but it's very early. It's basically a full abstraction proof and those are hard enough even when you don't have 'physics' as one of the layers.
@mario @david_chisnall In certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly. There's a bunch of this sort of thing that happens before any silicon is made. Takes a long time and is thus very expensive.
Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.
Jul 29, 2026, 2:34 PMIn certified software development--the ones I was involved with and read about anyway--this is done by a person who signs off that the implementation follows the spec correctly.
No it isn't. At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine. At least, not in any situation where liability may lead back to them, because it is never true (well, it's technically true for CompCERT, though with the all-bets-are-off-if-your-source-code-has-any-undefined-behaviour get-out-of-jail-free card).
Described situation was a demo during research phase sounds like. I hope they'd have found this before it made to production but yeah, no guarantees.
No, the point of the demo was that you would not find this. It was a tweak that was possible to make during back-end layout or to the GDSII after you've sent it to the fab, so a completely plausible supply-chain attack on a hardware security mechanism.
This kind of attack is easier on hardware than software, because you can at least run a compiled program on a simulator.
@david_chisnall @mario "At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine."
This is quite the straw man you've summoned. Didn't get any better either.
Later.
Jul 29, 2026, 2:36 PMI don't know what you think you're arguing with, but that's exactly the claim that you were making. You seem to be confusing formal verification with... something?
@david_chisnall @mario No dude. You completely made it up.
Jul 29, 2026, 2:38 PMI can only assume you're not reading the thread in context because you jumped into a middle of a conversation with a post about a problem with the concrete machine not being a faithful representation of the abstract machine that the proofs were constructed in to say that, in certified software development, people signed off on that.
Jul 29, 2026, 2:07 PM@mario @0xabad1dea @david_chisnall i can't seem to agree with this take, i am probably super wrong, but
i'll define a theorem prover as something that, when provided with a proof, can say with 100% surety whether the proof contains any mistake or not, and thus if it is valid, according to current database of proven methods
and if you agree with my definition, that should also include anything that isn't directly a part of the theorem prover, but still impact how it's output gets interpreted by the human, including,
- the software,
- the formal proof for that software,
- the hardware,
- the formal proof for that hardware,
- the model of the hardware, and
- even the human brain interpreting the results,
without having a 100% surety on all these terms, we can't say that, when theorem prover verifies a proof, the proof is true, with 100% surety.
Jul 29, 2026, 3:22 PM@mario @0xabad1dea @david_chisnall this kinda is making sense to me
basically, what i think you mean is
when we say "this proof is verified by xyz verifier", all the uncertainty that i mention gets put under the assumption that verifier isn't faulty
right?
i was going over whether that assumption can be true in my post, and what you're saying is once we add that assumption to our system, the proof becomes valid in that system, right?
Jul 29, 2026, 3:39 PM@mario @0xabad1dea @david_chisnall
> > 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
Jul 29, 2026, 3:43 PMGödel would like a word.
Jul 29, 2026, 3:46 PM@david_chisnall @mario @0xabad1dea and he'll probably take that word and assign a unique number to it