Meet Our Founder Grigore Rosu
Correct By Construction: Our Founder's Journey from Space Navigation Software to Blockchains
Grigore's career is defined by a focus on precision and reliability in software systems. After completing his PhD at UCSD, he joined NASA, where he worked on formal specification, semantics, and verification of flight and navigation software - some of the most mathematically and technically intensive programming in existence.
Journey to Pi Squared
2000
Journey Starts at NASA
After earning his PhD at UCSD, Grigore began his journey at NASA, where he worked on creating flight and navigation software for the space shuttle and spacecraft. His approach, known as "correct by construction," aimed to prevent errors before they could occur, which is critical in the environment of space exploration. This methodology helped ensure navigation systems operated accurately over vast distances, avoiding issues like the Mars Climate Orbiter crash. During this time, Grigore coined the term "Runtime Verification," laying the foundation for a new way to ensure the reliability of mission-critical systems.
After earning his PhD at UCSD, Grigore began his journey at NASA, where he worked on creating flight and navigation software for the space shuttle and spacecraft. His approach, known as "correct by construction," aimed to prevent errors before they could occur, which is critical in the environment of space exploration. This methodology helped ensure navigation systems operated accurately over vast distances, avoiding issues like the Mars Climate Orbiter crash. During this time, Grigore coined the term "Runtime Verification," laying the foundation for a new way to ensure the reliability of mission-critical systems.
2002
Academic Leadership at UIUC
In 2002, Grigore joined the faculty of the College of Engineering at the University of Illinois at Urbana-Champaign (UIUC). As a professor in the #2 CS program in the world, he teaches on the topics of blockchain, programming languages, formal methods, and software engineering. Grigore received several academic accolades, including the National Science Foundation's CAREER Award, Dean's award for excellence in research by the College of Engineering at UIUC, and the Automated Software Engineering IEEE/ACM Most Influential Paper Award. Grigore is also an IEEE fellow and AAAS fellow.
In 2002, Grigore joined the faculty of the College of Engineering at the University of Illinois at Urbana-Champaign (UIUC). As a professor in the #2 CS program in the world, he teaches on the topics of blockchain, programming languages, formal methods, and software engineering. Grigore received several academic accolades, including the National Science Foundation's CAREER Award, Dean's award for excellence in research by the College of Engineering at UIUC, and the Automated Software Engineering IEEE/ACM Most Influential Paper Award. Grigore is also an IEEE fellow and AAAS fellow.
2003
The K-Framework
Grigore, and his student Traian Serbanuta, invented the K-Framework in 2003. K enables the definition, or implementation of a formal semantics of a programming language in an intuitive and modular way. Once a semantics is complete, K provides a suite of tools including both an executable model and a program verifier.
Grigore, and his student Traian Serbanuta, invented the K-Framework in 2003. K enables the definition, or implementation of a formal semantics of a programming language in an intuitive and modular way. Once a semantics is complete, K provides a suite of tools including both an executable model and a program verifier.
2010
From Research to Real-World Impact
Grigore founded Runtime Verification (RV) in 2010. The company leveraged the formal semantics and verification techniques he developed at NASA and UIUC. Grigore fostered an environment where research and industry intersected by not only recruiting his students to join the company but also by partnering with academic peers. Runtime Verification collaborated with several prominent companies in the embedded systems space including Boeing, Toyota, and Denso. These collaborations were instrumental in developing several innovative products: RV Match, RV Monitor, and RV Predict. The work RV completed in the embedded space enabled it to become a leading Web3 security company. More on this to follow.
Grigore founded Runtime Verification (RV) in 2010. The company leveraged the formal semantics and verification techniques he developed at NASA and UIUC. Grigore fostered an environment where research and industry intersected by not only recruiting his students to join the company but also by partnering with academic peers. Runtime Verification collaborated with several prominent companies in the embedded systems space including Boeing, Toyota, and Denso. These collaborations were instrumental in developing several innovative products: RV Match, RV Monitor, and RV Predict. The work RV completed in the embedded space enabled it to become a leading Web3 security company. More on this to follow.
2013 to 2021
Numerous US Government Grants
Runtime Verification received several SBIR (Small Business and Investment Research) grants from the United States government. Like the contractual engagements with industry partners, the grants funded the advancement of the company's products; RV Mach, RV Monitor, and RV Predict, as well as the K-framework itself and multiple programming language semantics. In total the company received five stages of SBIR funding from the National Science Foundation (NSF) and eight stages of funding, spread across two grants, from the National Aeronautics and Space Administration (NASA).
Runtime Verification received several SBIR (Small Business and Investment Research) grants from the United States government. Like the contractual engagements with industry partners, the grants funded the advancement of the company's products; RV Mach, RV Monitor, and RV Predict, as well as the K-framework itself and multiple programming language semantics. In total the company received five stages of SBIR funding from the National Science Foundation (NSF) and eight stages of funding, spread across two grants, from the National Aeronautics and Space Administration (NASA).
2017 to Present
Bringing Formal Methods to Blockchain
Grigore and Runtime Verification (RV) entered Web3 in 2017. The company received the first ever security grant from the Ethereum Foundation as well as multiple grants from IOHK, the development firm behind the Cardano blockchain. Among the key projects funded by Charles Hoskinson and IOHK were KEVM, the formal semantics of the Ethereum Virtual Machine (EVM), and the IELE virtual machine, a variant of LLVM specialized to execute smart contracts on the blockchain.
The development of KEVM, along with the formal specification of the ERC-20 smart contract standard laid the foundation for the company to offer groundbreaking formal verification services to blockchain protocols and projects. Notable customers and engagements included Uniswap v1, the Ethereum Beacon Chain, the Ethereum Deposit Contract, and various projects for the Algorand, Cardano, MultiversX, and Tezos ecosystems.
Grigore and Runtime Verification (RV) entered Web3 in 2017. The company received the first ever security grant from the Ethereum Foundation as well as multiple grants from IOHK, the development firm behind the Cardano blockchain. Among the key projects funded by Charles Hoskinson and IOHK were KEVM, the formal semantics of the Ethereum Virtual Machine (EVM), and the IELE virtual machine, a variant of LLVM specialized to execute smart contracts on the blockchain.
The development of KEVM, along with the formal specification of the ERC-20 smart contract standard laid the foundation for the company to offer groundbreaking formal verification services to blockchain protocols and projects. Notable customers and engagements included Uniswap v1, the Ethereum Beacon Chain, the Ethereum Deposit Contract, and various projects for the Algorand, Cardano, MultiversX, and Tezos ecosystems.
2023
Founding of Pi Squared
Grigore launched Pi Squared in late 2023 as a spin-off from Runtime Verification. Pi Squared aims to change a world beset by deep fragmentation caused by programming language barriers from Web2 to Web3; ecosystem barriers preventing true cross-chain interoperability; and trust barriers in cloud computing. The company is building groundbreaking products to break these barriers; The Universal Language Machine (ULM) empowers developers to write and execute programs in any language on any blockchain; The Universal Settlement Layer (USL) is a modular and universal protocol set that redefines cross-chain interoperability; and lastly Proof of Proof is a universal verifiable computing framework based on formal methods and zero-knowledge technologies.
Grigore launched Pi Squared in late 2023 as a spin-off from Runtime Verification. Pi Squared aims to change a world beset by deep fragmentation caused by programming language barriers from Web2 to Web3; ecosystem barriers preventing true cross-chain interoperability; and trust barriers in cloud computing. The company is building groundbreaking products to break these barriers; The Universal Language Machine (ULM) empowers developers to write and execute programs in any language on any blockchain; The Universal Settlement Layer (USL) is a modular and universal protocol set that redefines cross-chain interoperability; and lastly Proof of Proof is a universal verifiable computing framework based on formal methods and zero-knowledge technologies.