Tagged “rocq”

• Neurosymbolic C++ Verification in Rocq

  May 12, 2026

  Neurosymbolic capabilities have revolutionized the entire software development process, from requirements engineering and code development to testing and maintenence. In this talk, we will present our work integrating agentic techniques into the Brick C++ verification platform. Our approach combines algorithmic reasoning techniques, e.g. concurrent separation logic with sophisticated automation, proof search strategies, etc., with higher-level insights and probabilistic inference provided by LLMs. Our experience demonstrates that combining these technologies enables scalable reasoning for real-world programs.

  rocq c++ program verification separation logic brick templates skylabs-ai

• Verification of Templated Code in C++

  Jan 17, 2026

  C++ templates are used pervasively and a major blocker for applying verification to real code bases. We present an approach to verifying templated code that avoids enlarging the trusted computing base of the C++ semantics. Our approach uses a shallowly embedded logic that enables reasoning about unresolved symbols as hygienic macros. We have applied our approach to verify several small function templates and used their proofs to derive proofs for concrete instantiations of these functions.

  rocq c++ program verification separation logic brick templates skylabs-ai

• Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic

  Jan 17, 2026

  We present the current progress of specifying and verifying the NOVA microhypervisor at BlueRock Security. We carry out these tasks using the BRiCk C++ program logic and verification tools, building on top of the Iris framework for concurrent separation logics (CSLs), in Rocq. We found that the use of CSLs has enabled us to carry out highly modular specifications and verifications of even sophisticated, fine-grained concurrent algorithms in NOVA. We believe this is a significant step forward over other hypervisor verification projects that are either limited to single-threaded verification or are highly non-modular.

  rocq c++ program verification separation logic brick concurrency nova hypervisor skylabs-ai bluerock-security

• Recursive Mutexes in Separation Logic

  Jan 17, 2026

  Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this abstract, we develop the same styles of specifications for _recursive_ mutexes, a common variant of mutexes in object-oriented languages like C++ and Java. A recursive mutex can be acquired any number of times by the same thread, and our specifications treat all acquires/releases uniformly, with clients only needing to determine whether they hold the mutex when accessing the lock invariant.

  rocq c++ program verification separation logic brick concurrency skylabs-ai

• Towards an Axiomatic Basis for C++

  Jul 5, 2020

  @inproceedings{malecha2020-axiomatic-cpp, title={Towards an {A}xomatic {B}asis for {C++}}, author="Gregory Malecha and Abhishek Anand and Gordon Stewart", booktitle={The 11th Coq Workshop}, lo...

  rocq c++ program verification separation logic axiomatic semantics

• Interaction Trees: Representing Recursive and Impure Programs in Coq

  Jan 24, 2020

  @article{xai2020-interaction-trees, author = {Xia, Li-yao and Zakowski, Yannick and He, Paul and Hur, Chung-Kil and Malecha, Gregory and Pierce, Benjamin C. and Zdancewic, Steve}, title = {Interaction...

  rocq coinduction denotational semantics

• A Denotational Semantics for an Imperative Language

  Oct 21, 2018

  In my last post I presented an implementation of a fixpoint combinator in Coq. In this post, I'm going to show how that technique can be used to give a compositional denotational semantics to Imp, a simple imperative programming language. I'm not going to pretend to cover all the corner cases of C in this post (perhaps a future post), but rather will focus on the general recipe for defining semantics using co-inductive effects.

  rocq interaction trees extensible effects semantics denotational semantics

• Compositional Non-termination without Fuel

  Aug 27, 2018

  @inproceedings{malecha-nontermination, title={Compositional {N}on-termination without {F}uel}, authors={Gregory Malecha}, year={2018}, month=Aug, conference={NEPLS'18}, location={Cambridge...

  rocq coinduction denotational semantics

• Compositional (Co-inductive) Recursion in Coq

  Jun 29, 2018

  There have been several different articles that advocate for the use of denotational semantics, where we give a function from the syntax to another language that we already understand. In Coq, the target language is often Gallina. However, because all Gallina programs terminate, we can't give a direct interpretation of non-terminating programs. An alternative is to give a denotation of your source language through a co-inductive definition of traces. The problem with this is that co-recursion is notoriously non-compositional in Coq. The paco work provides a compositional proof rule for co-inductive types, but the is no similar definition for co-inductive definitions. In this post I'm going to explain how to build a general recursion combinator in Coq that is completely composable- a surprisingly difficult problem that I pondered for a while in grad school.

  rocq coinduction extensible effects semantics general recursion

• Speeding Up Proofs with Computational Reflection

  Jun 5, 2017

  One of the biggest complaints about proof assistants such as Coq is performance. Large proofs can be slow to both construct and to check which reduces the "interactive" nature of interactive proof assistants and makes maintenance painful. However, while the richness of dependent type theory is partially to blame for this slowness, it also allows us to use computational reflection to extend the proof checker to build and check proofs quickly. In computational reflection, we convert proof objects in to computations and run them on Coq's bytecode virtual machine to achieve orders of magnitude improvements in proof construction and checking. In this talk I walk through how computational reflection works using a few small examples. Time permitting, I will discuss how these ideas can be used to build larger scale reflective automation (the MirrorCore project) including an Ltac-like DSL for reflective automation that provides some of the speed benefits of computational reflection without some of the drawbacks.

  rocq verification automation reflection

• Challenge: member_heq_eq

  Feb 22, 2017

  Working on a polymorphic version of MirrorCore I have been working a lot with heterogeneous lists and proof-relevant membership. The later is the source of this challenge problem.

  rocq challenge dependent types

• Qed Considered Harmful

  Feb 18, 2017

  Coq provides two ways to finish definitions Qed and Defined. The former is meant for "proofs" and makes the definition opaque while the later is meant for "definitions" and leaves the definition transparent. While the "proof" and "definition" dicotomy initially makes a lot of sense to users, but as users start to use dependent types more and more, they realize that the distinction is quite arbitrary, in which case, should we abandon Qed? In this post, I argue that yes abandoning Qed is a perfectly sensible thing to do.

  rocq dependent types qed

• Predicate Monads

  Jan 21, 2017

  @inproceedings{westbrook-predicate-monads, title={Predicate {M}onads: A {F}ramework for {P}roving {G}eneric {P}roperties of {M}onadic {P}rograms via {R}ewriting}, authors={Edwin Westbrook and Greg...

  rocq monads verification logic

• Modular Deductive Verification of Sampled-Data Systems

  Oct 14, 2016

  Unsafe behavior of cyber-physical systems can have disastrous consequences, motivating the need for formal verification of these kinds of systems. Deductive verification in a proof assistant such as Coq is a promising technique for this verification because it (1) justifies all verification from first principles, (2) is not limited to classes of systems for which full automation is possible, and (3) provides a platform for proving powerful, higher-order modularity theorems that are crucial for scaling verification to complex systems. In this paper, we demonstrate the practicality, utility, and scalability of this approach by developing in Coq sound and powerful rules for modular construction and verification of sampled-data cyber-physical systems. We evaluate these rules by using them to verify a number of non-trivial controllers enforcing safety properties of a quadcopter, e.g. a geo-fence. We show that our controllers are realistic by running them on a real, flying quadcopter.

  rocq veridrone cyber-physical

• Experimenting with Mtac

  Apr 18, 2016

  I spent some time experimenting with Mtac and figured that I'd write a little bit about my experience. Mtac is a tactic language for Coq where you get write Gallina terms that manipulate raw Coq syntax through a monadic interface.

  rocq Mtac

• Towards Foundational Verification of Cyber-physical Systems

  Apr 11, 2016

  The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using high-level reasoning techniques such as Lyapunov functions and model checking. In this paper we present VeriDrone, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VeriDrone is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safety-critical systems and ensuring interesting properties at all levels of the stack.

  rocq veridrone cyber-physical

• PhD Defense: Extensible Proof Engineering in Intensional Type Theory

  Mar 22, 2016

  You can now watch my thesis defense on computational reflection in intensional type theory. Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).

  rocq computational reflection mirror-core rtac

• Using SMT Solvers in Coq 8.5

  Mar 16, 2016

  During my post-doc at UCSD I've been working on verifying cyber-physical systems in the VeriDrone project. Cyber-physical systems are just systems that interact with the real world (think quadcopters, cars, planes, hydro-electric dams, and robots). The interesting thing about verifying cyber-physical systems in Coq is that they require a lot of reasoning about continuous mathematics, real numbers, differential equations, and all that. Coq does a great job at all of the discrete reasoning that we do (see my previous blog post on embedding logics in Coq) but at the end of all the nice theory, problems often boil down to mundane reasoning about real arithmetic. In this post I'm going to discuss a plugin that I wrote to call SMT solvers from Coq.

  rocq plugins SMT rocq

• Rtac: Reflective Tactics in Coq

  Feb 20, 2016

  In this post I'm going to discuss Rtac the reflective tactic language that I developed as a central piece of my dissertation. The results there show how reflective tactics can be a game-changer in the ability to build very efficient automation. For comparison, the automation that I'm going to write in this post is a monoidal cancellation procedure and at the end of the post we'll see that it scales substantially better than Ltac, e.g. on larger problems it is almost 2 orders of magnitude faster than Ltac.

  rocq mirror-core rtac computational reflection

• Extensible and Efficient Automation through Reflective Tactics

  Jan 1, 2016

  Foundational proof assistants simultaneously offer both expressive logics and strong guarantees. The price they pay for this flexibility is often the need to build and check explicit proof objects which can be expensive. In this work we develop a collection of techniques for building reflective automation, where proofs are witnessed by verified decision procedures rather than verbose proof objects. Our techniques center around a verified domain specific language for proving, Rtac, written in Gallina, Coq's logic. The design of tactics makes it easy to combine them into higher-level automation that can be proved sound in a mostly automated way. Furthermore, unlike traditional uses of reflection, Rtac tactics are independent of the underlying problem domain, which allows them to be re-tasked to automate new problems with very little effort. We demonstrate the usability of Rtac through several case studies demonstrating orders of magnitude speedups for relatively little engineering work.

  rocq rtac computation reflection automation

• Embedding Logics in Coq

  Dec 18, 2015

  Coq comes with a powerful, built-in logic (Gallina) with features such as inductive and dependent types, recursion, etc. However, most uses of Coq don't study its theory, but rather use it as a foundation to reason about something else. A few examples come to mind:

  rocq tutorial

• The Core of Computational Reflection

  Oct 3, 2015

  Computational reflection is a technique for extending proof assistants with efficient, domain-specific automation. There are a lot of interesting ideas in computational reflection but in this blog post I'm just going to cover a simple example, proving evenness of large constants. This example is purposefully extremely simple, and computational reflection is certainly capable of doing a lot more, but the very key pieces are here.

  computational reflection rocq tutorial

• Using Dependent Types and Tactics to Enable Semantic Optimization of Language-Integrated Queries

  Aug 4, 2015

  Semantic optimization -- the use of data integrity constraints to optimize relational queries -- has been well studied but, owing to limitations in how SQL handles constraints, has not often been applied by mainstream RDBMSs. In a language-integrated query setting, however, the query provider is free to rewrite queries before they are executed on an RDBMS. We show, using Coq as our ambient language, how to use dependent types to represent a well known class of constraints -- embedded, implicational dependencies -- and how Coq tactics can be used to implement a particular kind of semantic optimization: tableaux minimization, which minimizes the number of joins required by a query.

  rocq refinment databases optimization

• Extensible Proof Engineering in Intensional Type Theory

  Feb 1, 2015

  We increasingly rely on large, complex systems in our daily lives---from the computers that park our cars to the medical devices that regulate insulin levels to the servers that store our personal information in the cloud. As these systems grow, they become too complex for a person to understand, yet it is essential that they are correct. Proof assistants are tools that let us specify properties about complex systems and build, maintain, and check proofs of these properties in a rigorous way. Proof assistants achieve this level of rigor for a wide range of properties by requiring detailed certificates (proofs) that can be easily checked.

  In this dissertation, I describe a technique for compositionally building extensible automation within a foundational proof assistant for intensional type theory. My technique builds on computational reflection---where properties are checked by verified programs---which effectively bridges the gap between the low-level reasoning that is native to the proof assistant and the interesting, high-level properties of real systems. Building automation within a proof assistant provides a rigorous foundation that makes it possible to compose and extend the automation with other tools (including humans). However, previous approaches require using low-level proofs to compose different automation which limits scalability. My techniques allow for reasoning at a higher level about composing automation, which enables more scalable reflective reasoning. I demonstrate these techniques through a series of case studies centered around tasks in program verification.

  mirror-core rtac rocq computational reflection

• Rtac: A Fully Reflective Tactic Language

  Jan 18, 2015

  @inproceedings{malecha2015rtac-coqpl, title="{Rtac}: A Fully Reflective Tactic Language", author="Gregory Malecha and Jesper Bengtson", month="January", year="2015", booktitle="CoqPL'15" }...

  rtac rocq computational reflection automation

• Automating Abstract Logics (a.k.a. Implementing Reflective Tactics)

  Jul 16, 2014

  @article{malecha2014automating, title="Automating Abstract Logics", author="Gregory Malecha and Jesper Bengston and Adam Chlipala", booktitle={The 6th Coq Workshop}, location={Vienna, Autria},...

  mirror-core rocq computational reflection automation talk

• Compositional Computational Reflection

  Jul 14, 2014

  Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof- generating tactic language such as Ltac. This composition, however, comes at the cost of both larger proof terms and redundant preprocessing. In this work, we propose a methodology for writing composable reflective procedures that solve many small tasks in a single invocation. The key technical insights are techniques for reasoning semantically about extensible syntax in intensional type theory. Our techniques make it possible to compose sound procedures and write generic procedures parametrized by lemmas mimicking Coq’s support for hint databases.

  mirror-core rocq computational reflection automation

• MirrorShard: Proof by Computational Reflection with Verified Hints

  May 28, 2013

  We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and checking of proofs, we use verified-correct procedures with Coq soundness proofs. Though they are internalized in Coq's logic, our provers support sound extension by users with hints over new domains, enabling automated reasoning about user-defined abstract predicates. We maintain soundness by developing an architecture for modular packaging, construction, and composition of hint databases, which had previously only been implemented in Coq at the level of its dynamically typed, proof-generating tactic language. Our provers also include rich handling of unification variables, enabling integration with other tactic-based deduction steps within Coq. We have implemented our techniques in MirrorShard, an open-source framework for reflective verification. We demonstrate its applicability by instantiating it to separation logic in order to reason about imperative program verification.

  mirror-shard rocq computational reflection automation

• Reflecting Modular Automation

  Jan 18, 2013

  @unpublished{malecha2013reflecting, title="Reflecting Modular Automation", author="Gregory Malecha", month="January", year="2013", url={http://gmalecha.github.io/publication/2013/01/18/refle...

  talk rocq mirror-shard computational reflection

• Compiling Coq in Coq

  Jan 17, 2013

  @unpublished{malecha2013compiling, title="Compiling {C}oq in {C}oq", author="Gregory Malecha", month="January", year="2013" }...

  rocq compilation

• Building Bedrock: Verifying a Program Verifier

  Aug 12, 2012

  We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and checking of proofs, we use verified-correct procedures with Coq soundness proofs. Though they are internalized in Coq's logic, our provers support sound extension by users with hints over new domains, enabling automated reasoning about user-defined abstract predicates. We maintain soundness by developing an architecture for modular packaging, construction, and composition of hint databases, which had previously only been implemented in Coq at the level of its dynamically typed, proof-generating tactic language. Our provers also include rich handling of unification variables, enabling integration with other tactic-based deduction steps within Coq. We have implemented our techniques in MirrorShard, an open-source framework for reflective verification. We demonstrate its applicability by instantiating it to separation logic in order to reason about imperative program verification.

  mirror-shard rocq computational reflection automation

• Mechanized Verification with Sharing

  Sep 1, 2010

  We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures with more complex sharing patterns. This problem is compounded by some higher-order patterns, such as stateful iterators and visitors, where multiple clients need to share references into a data structure. We show how both styles of sharing can be achieved without sacrificing abstraction using mechanized reasoning about fractional permissions in Hoare Type Theory.

  rocq separation logic ynot

• Toward a verified relational database management system

  Jan 20, 2010

  We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for finite relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.

  ynot rocq b+ tree separation logic

• Trace-based verification of imperative programs with I/O

  Jan 15, 2010

  In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants.

  ynot separation logic rocq verification

• Effective interactive proofs for higher-order imperative programs

  Aug 31, 2009

  We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

  ynot separation logic rocq verification