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