Mission and Vision logoMission and Vision

Our mission is accessible trustworthy computing. We accomplish it by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning.

Relevant links

  • Matching logic [link]
    • Matching mu-logic, LICS'19 [paper]
    • Matching logic, LMCS'17 [paper]
    • Generating matching logic proof objects for program execution, CAV'21 [paper]
    • Generating matching logic proof objects for formal verification, OOPSLA'23 [paper]
  • Runtime verification
    • Publications on security audit and formal verification of protocols, virtual machines, and smart contracts [link]
    • Past presentations [link]
    • Videos and talks [link]
    • RV Research [link]
  • Related tools:
    • K Framework [link]
    • The 200-line matching logic proof checker [link]
    • ERCx [link]
    • RV-Match [link] and RV-Monitor [link]
    • Foundry [link]
    • Metamath [link]