Mission-critical computer systems rely on secure information sharing and interoperability—and failure can have disastrous consequences. A world leader in the formal verification of computer systems, SRI develops and offers specifications for high-assurance systems software and hardware platforms.

• Prototype Verification System: a tool that provides rigorous assurance of correctness for mission-critical systems

• Yices: a high-assurance software program that decides the satisfiability of propositional formulas containing uninterpreted function symbols

• Symbolic Analysis Laboratory: an environment that uses transition relations to explore and analyze concurrent systems