We are very happy to announce that we are starting our first research project!
The project marks the start of our partnership with Runtime Verification (RV), and concerns the Lean formalization of Matching Logic (ML), a unifying logic for program specification and verification introduced by RV founder and CEO Grigore Roșu and his collaborators, which also serves as the theoretical foundation of the 𝕂 Semantic Framework. The project goals are to enhance the ML ecosystem by adding Lean support and to ultimately offer the 𝕂 ecosystem a trusted interactive formal verification environment.
For more information, see the project page.