Kestrel Institute is a non-profit computer science research center, located in the Stanford Research Park in Palo Alto, California.

Our research spans formal methods, program synthesis and refinement, program analysis and verification, theorem proving, and planning.

Kestrel can provide formal methods assistance for software projects of all types. Our techniques include:

  • Correct-by-Construction Code Synthesis
    • Refine specification to code (C, Java, etc.)
    • Correctness proved by ACL2 theorem prover
    • Can produce many diverse variants
  • Formal Verification of Existing Code
    • Lift code into logic and prove properties
    • Equivalence check vs spec or golden model
    • Answer yes/no questions about code
  • Formal Analysis of System Models
    • Formalize architecture, requirements, etc.
    • Prove properties of the models
    • Later, prove that code implements the models
  • Verified Program Transformations
    • Restructure code to increase security
    • Compartmentalize, harden, change language
    • Proofs ensure no errors introduced
  • Formal Unit Testing
    • Evolve unit tests into powerful, automatic proofs

To learn more, contact us or see this summary of our technology.

Kestrel’s sponsors and customers include DARPA, DoD, IARPA, AFRL, AFOSR, ONR, NASA, NSF, GE, the Ethereum Foundation, the Decentralization Foundation, the Tezos Foundation, and NRI Secure. Kestrel’s collaborators include Stanford University, Vanderbilt University, UT Austin, MIT, University of Michigan, University of Virginia, Sandia National Laboratories, CACI / Next Century, and Collins Aerospace.