Protocol Labs Research
About
People
Research
Outreach
Blog

Latest work

2020.12.9 / Publications

Improving system resilience through formal verification of transactive energy controls

Formal verification tools such as TLA+ allow errors to be uncovered through exhaustive exploration of reachable states, and are the gold standard for ensuring resilience in software systems. In particular, these methods can be used to identify error states emerging from precise interactions between multiple subsystems that would occur only after long periods of testing, operation, or stacked error conditions.