Future Vision: We are developing safety layer architectures (SLAs) to plug into generative AI systems. These SLAs employ formal methods and proof assistants to ensure correctness and safety for AI input/output layers. In a sense, we are using the power of genAi models to help guide AI systems through their critical decision points and prove correctness along their pathways. In our SLAs, LLMs generate formal proofs using dependently typed languages for proof verification and employing heuristic techniques for iterative proof repair and refinement.

Program Overview: Our R&D program is designed to test critical use cases in important verticals with safety minded genAi industry participants and partners. Our process first abstracts tool layers in a unified proof of concept (PoC) for the underlying tool set and configuration. Later, we produce a PoC for each of the critical and important use cases we test with Industry Partner participants, highest level. They can gauge and customize ways of assuring output safety for their specific use case(s) as part of the program (and also receive white glove installation). This way, in addition to tech transfer, each highest level participant receives their PoC as a demonstration of the efficacy of using this tech to enhance the safety of their specific systems.

R&D Live: Our program is organized for a series of live interactive virtual events coinciding with code releases and test tooling updates and releases. A stearing committee of members from the Industry Partner level will meet regularly. Input from sponsors will also be invited. Sponsorship doubles our live community and enhances the value of our R&D.