Formal modeling of systems based on E/CapTP/(Water)Ken/Cap'n Proto ideas

One thing I've observed about distributed object capability systems is that
things like handling errors and ensuring messages don't get dropped is
generally described in terms of "guidelines". I'm thinking things like COVR
here.

This gives a developer a lot of expressiveness and flexibility, but not a
lot of assurances that making a single misstep anywhere will break
everything.

Tools like temporal logic (with mechanically checked proofs) and (formally
modeled) replicated state machines seem like they could help here, and
ensure that all potential failure modes are handled in some way (even if
it's surfacing an error). I'm thinking of something like TLA+ here, at
least to model check an approach like COVR.

Have there been any attempts at applying temporal logic to proving the
correctness of object capability systems?

-- 
Tony Arcieri

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk