Creating Human Interpretable Experiences From Formal Proofs
Software users rely on static, often difficult-to-navigate documentation, checklists, and training materials to understand the software systems they use. A system’s true behavior and capabilities may be opaque or inaccessible, leaving non-expert users with gaps in their ability to adapt settings or interpret outputs under changing conditions. These gaps hinder users’ ability to improvise or repurpose systems to solve problems as they arise.
The LUCID program seeks to create human interpretable experiences from formal proofs that verify software behavior. The program is based on the insight that formal proofs encode system knowledge in a compact, symbolic form, yet assured systems make no ongoing use of the information captured in the proof itself. That information is accessible only to formal methods subject matter experts. If it can be made accessible to non-expert users, it could help solve problems within intended use parameters and also potentially reveal safe new ways to adapt the system for novel challenges.
LUCID aims to demonstrate that software proofs encode system knowledge, and seeks to develop decision support tools that extract, communicate, and use that knowledge to change the way humans interact with mission-critical software. In so doing, the program seeks to bridge the gap between formal technical assurance and mission-ready operational decisions for high-stakes scenarios.
Success in the LUCID program requires overcoming challenges in addressing semantic gaps, temporal reasoning, and compositional reasoning at scale.
The LUCID program anticipates four phases, with Phase 1 focused on a proof of concept that demonstrates a clear, traceable path from a software proof to user insight.
