Mission 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]