Galois Technologies

Galois specializes in the research and development of innovative new approaches and technologies that provide information assurance for challenging systems and software environments.

Our world-class researchers and engineers build upon a solid foundation of mathematics and science to address the most challenging problems today:

  • Applied formal methods
  • Cryptography
  • Language design and compilation techniques
  • Security and trusted computing (excluding crypto)
  • Systems of systems
  • Hardware and cyber-physical systems
  • Cross-domain security
  • Programming at Internet scale

By addressing performance, trust relationships, and security at all levels of the software stack, we provide you with multiple active defense and protection mechanisms built on a solid foundation of math and computer science. Our technology solutions enable flexible security strategies at an architectural or component level, help address insider threats and detect attack "command and control" patterns.

And, with our safety and security verification and validation (V&V) tools, you can feel confident that our technologies meet specifications and fulfill their intended purpose:

  • Information flow analysis
  • Hardware verification
  • Driver systems, kernel design
  • Type systems and formal mathematical analysis of software
  • Automated software analysis for a wide range of properties
  • Custom V&V and analysis tools

At Galois, we embrace open innovation. We believe the open innovation model for research and development is the most effective means to keep up with disruptive technology advancements. We also continually look to build paths to commercialization through new and existing strategic partnerships.

Helping to Standardize Theory Engineering by Archiving Proofs as Theory Packages

This is a short video about theory engineering techniques to support interactive theorem proving for tackling large formalization and verification projects. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.

Collaborate with Us

Licensing - Obtain a license for one of our advanced technologies.

Research & Development - Solve your toughest problems by exploring new approaches with us.

Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.

Let's Work TogetherStart the Conversation >>