Media Kit
Runtime Verification Inc is an American startup with a global presence, applying formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain. We work with infrastructure builders to provide testing and verification services and tools.
The company was founded in 2010 by pioneers in the academic field and it gained a select roster of clients in the embedded systems space (NASA, Boeing, Toyota, Denso, NSF, DARPA) and the blockchain (Algorand, Cosmos, MultiversX, Ethereum, Gnosis, IOHK, Maker, PlatON, Polkadot, Tezos, and Uniswap), among many others.
Located between Urbana (the home of the University of Illinois) and its sister city of Champaign, our headquarter is roughly 2.5 hours South of Chicago, 2 hours West of Indianapolis, and 3 hours North of St. Louis. In 2018, Champaign scored the #1 spot in the Best Cities for Recent College Grads ranking, and #2 overall (out of 42 communities) in the Silicon Prairie region.
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. K allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.
Our symbol, the two drops (blue and yellow), represent the specification and the implementation. During verification we prove that the two are tightly connected, therefore two rigidity points (RV-Match). For dynamic analysis (RV-Predict and RV-Monitor) some aspects get verified, but not all the implementation, therefore one rigidity point. The two drops mirror each other, but not perfectly.
