On 22 Apr 2021, at 13:38, Gerwin Klein
this might sound counter-intuitive, but the glue-code proofs bring fairly low return of
investment in terms of assurance vs proof effort. This is because they are about generated
code, i.e. code that has systematic errors instead of random errors, because they have to
assume well-behaved component code (running in the same address space as the glue code),
which is only satisfied for fairly high-assurance components (i.e. needs at least a proof
The one case where the glue code verification adds real value is if the connector is
between two verified components, where it guarantees that the connection is functionally
equivalent to a function call. As the number of verified components increase, this will
become more of an issue.
So we would welcome someone redoing those proofs for the standard connectors, it’s just
not high enough on our priorities (for now).