CertiuCOS2

A Rocq framework for verifying preemptive operating-system kernels, with a uC/OS-II case study.

CertiuCOS2 provides the models, program logic, and proof automation needed to connect kernel implementations to abstract API specifications. Its relational separation logic supports modular reasoning about shared kernel data, scheduling, context switches, and interrupts. Individual API and interrupt-handler proofs are combined into a system-level refinement result.

The project is intended for researchers and developers studying OS verification, extending verified kernel services, or reusing separation-logic proof automation. It includes a mechanized uC/OS-II development and is maintained in Rocq, formerly Coq. The framework is presented in “A Practical Verification Framework for Preemptive OS Kernels” (CAV 2016).

Paper · Technical report · Architecture guide · Development guide

Architecture

Figure 1 from the CAV 2016 paper, reproduced from the original embedded image. The figure uses the name Coq; the project now builds with Rocq. Figure source and attribution.

The four parts work together:

• A. Kernel models: a low-level language models C-like code, context switches, and interrupts; a high-level language describes abstract operations and configurable scheduling policies.
• B. Refinement logic: relational assertions and proof rules connect the two models. The soundness theorem turns local proofs into contextual refinement, relating observable client behavior across the concrete and abstract kernels.
• C. Proof automation: reusable tactics support forward reasoning, separation-logic entailments, and domain-specific proof obligations.
• D. uC/OS-II verification: the framework is applied to interrupts, priority-based scheduling, message queues, mutexes, semaphores, and mailboxes.

The system theorem ucos_correct establishes GOOD_OS low_level_os_code os_spec ucos_init, using the framework's Soundness theorem. The architecture guide maps these results to the source modules.

Verification status: all 224 Rocq modules compile and pass recursive kernel checking. Results depend on the recorded assumptions, including the inconsistent MemoryNotFull axiom. See Assumptions and limits for the scope of these results.

What is included

The current code and specification tables contain 25 APIs, 10 internal helpers, and 2 interrupt handlers.

Area	Examples	Proof directory
Message queues	accept, create, delete, pend, post, get message	msgqueue
Mailboxes	accept, create, delete, pend, post	mailbox
Semaphores	accept, create, delete, pend, post	semaphore
Mutexes	accept, create, delete, pend, post	mutex
Time	delay, read time	time
Tasks	create, delete; ready and waiting deletion cases	task
Kernel internals and interrupts	scheduler, event-list operations, TCB initialization, time tick, interrupt exit	oscore

The repository also contains priority-inversion proofs for a dedicated abstract model. These require explicit client and initialization conditions, including good_client_code and no_nest_client; the unbounded-priority-inversion theorem additionally requires PREEMP. This separate proof branch uses its own os_spec' and is included in the full build. Arbitrary nested mutex use is outside these guarantees.

Build and verify

The validated configuration is Rocq 9.2.0, Stdlib 9.1.0, and OCaml 5.4.0 on Apple Silicon macOS. You also need Git, make, and Python 3. A clean build on the validation machine with 16 GiB RAM and two jobs took approximately 21 minutes; recursive checking took approximately 5 minutes. Other platforms have not been validated by this port.

With opam installed, prepare an isolated switch:

# Run once if opam has not been initialized:
opam init --bare --no-setup

opam switch create certiucos2 ocaml-base-compiler.5.4.0
opam install --switch=certiucos2 rocq-core.9.2.0 rocq-stdlib.9.1.0
eval "$(opam env --switch=certiucos2 --set-switch)"

git clone https://gitcode.com/brightfu/CertiuCOS2.git
cd CertiuCOS2
make version
make -j2
make check
make audit

make compiles every .v file under coqimp/framework, coqimp/tactics, and coqimp/certiucos to ordinary .vo files. make check recursively checks all these modules and their dependencies with the Rocq kernel. make audit compares assumption declarations and existing aborted-proof counts with the upstream baseline and rejects admitted proofs and known checking bypasses.

The Rocq launcher uses rocq on PATH, or the executable selected by CERTIUCOS_ROCQ. Activate the matching opam environment when selecting a specific installation.

Use one or two jobs initially. Some proof files require substantial memory. Deprecation and notation warnings remain visible; checking is never bypassed with .vos, -quick, -admit, or disabled kernel checks.

# Rebuild from scratch:
make clean
make -j2

# Work on one API and its dependencies:
make -C coqimp -j2 certiucos/proofs/msgqueue/OSQAcceptProof.vo

After changes, run make check and make audit as well. Use the root Makefile or coqimp/Makefile. For an editor, open coqimp, use its _CoqProject, and select the same opam switch. The development guide covers targeted builds and proof debugging.

Explore the code

coqimp/
  framework/
    model/       Memory, language syntax, and operational semantics
    logic/       Relational assertions and inference rules
    proof/       Simulation, rule soundness, and OS correctness
    auxlibs/     Integer/map libraries and Rocq compatibility names
  tactics/       Symbolic execution, separation, arithmetic, and OS tactics
  certiucos/
    code/        Manually encoded kernel implementations
    spec/        Abstract APIs, internal contracts, invariants, and PIF
    inline/      Inline code helpers and their proof support
    ucos_lib/    Reusable lemmas about kernel data structures and operations
    proofs/      API, interrupt, and system integration proofs
uCert-code/      C/assembly reference sources and build files
docs/            Architecture, contributor workflow, and verification records
scripts/         Rocq launcher and assumption audit

Start with a small API such as OSQAccept:

1. Read its implementation in os_q.v.
2. Find its abstract behavior in abs_op.v and its registration in os_spec.v.
3. Read the relevant invariants in os_inv.v and helper lemmas in OSQAcceptPure.v.
4. Follow OSQAcceptProof.v, observing how hoare forward, separation tactics, and abstract-operation rules discharge obligations.
5. See how ucos_correct.v combines that proof with the other APIs.

Two similarly named specifications serve different purposes: lowercase os_spec describes abstract APIs, interrupts, and scheduling; uppercase OS_spec, defined in ifun_spec.v, contains internal helper-function contracts. The architecture guide explains their connections and the theorem dependency path.

Extend the project

For a new API or a behavior change, update the concrete implementation, abstract specification, affected invariants, proof lemmas, API proof, and top-level registration together. A passing isolated lemma is only one step: finish by compiling the affected integration theorem and running the complete build, kernel check, and assumption audit.

The development guide gives the file-by-file workflow and proof-debugging conventions. CONTRIBUTING.md describes review and language requirements. Maintain README files, developer documentation, explanatory comments, commit messages, and contribution discussions in English. Keep established Rocq identifiers stable unless a change is justified and its dependencies are updated.

Useful maintenance directions include resolving the inherited memory-model inconsistency, reducing dependence on deprecated tactics and library names, improving modularity of the larger API proofs, and extending specifications with explicitly stated assumptions. Changes to the memory model or the logic require revisiting their soundness proofs and dependent results.

Assumptions and limits

Known memory-model inconsistency

memory.v declares:

Axiom MemoryNotFull : forall m, ~ FullMemory m.

Memory is modeled as an unrestricted function. A constant function returning a present cell at every address is therefore a full memory, contradicting this axiom, which is an actual dependency of ucos_correct. A consistent memory model and the associated proof repairs are still required before these results can support an unconditional correctness claim.

Other boundaries

• The development also uses classical reasoning, extensionality, proof irrelevance, and equality-related assumptions. Inspect the main theorem's assumptions and full kernel context summary.
• Kernel implementations are manually encoded in Rocq. Translation from the reference C/assembly sources, compilation, and execution on physical hardware are outside the checked source-model theorem. Context-switch and interrupt primitives are modeled explicitly. The reference sources are not built by the Rocq Makefile.
• The modeled C subset includes integers, arrays, structures, conditionals, loops, pointers, and defined pointer-offset operations. It has no union, floating-point, or for constructor, and integer-to-pointer casts are unsupported. Kernel and client resources obey the model's separation conditions. See the actual syntax and semantics before extending the subset.
• Scheduling and priority-inversion claims have their own premises. They do not supply measured execution-time or deadline bounds.
• The upstream tree includes exploratory Abort commands and abstract module parameters. The audit preserves their baseline counts and declarations. It is a source-level regression check, while make check validates proof terms under the recorded assumptions.

The verification record records the validated toolchain, commands, results, and source hashes. upstream-assumptions.json records the imported assumption baseline.

Research and citation

Please cite the research paper when using this framework, and record the repository commit and Rocq toolchain for reproducibility:

Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. CAV 2016, Part II, LNCS 9780, pp. 59–79. Springer. DOI: 10.1007/978-3-319-41540-6_4.

@inproceedings{XuFFZZL2016,
  author    = {Fengwei Xu and Ming Fu and Xinyu Feng and Xiaoran Zhang
               and Hui Zhang and Zhaohui Li},
  title     = {A Practical Verification Framework for Preemptive {OS} Kernels},
  booktitle = {Computer Aided Verification (CAV 2016), Part II},
  editor    = {Swarat Chaudhuri and Azadeh Farzan},
  series    = {Lecture Notes in Computer Science},
  volume    = {9780},
  pages     = {59--79},
  year      = {2016},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-41540-6_4}
}

The proof automation builds on earlier separation-logic tactics, including Jingyuan Cao, Ming Fu, and Xinyu Feng, “Practical Tactics for Verifying C Programs in Coq”, CPP 2015, pp. 97–108 (DOI, author-hosted paper).

The paper, technical report, and slides explain the research. Machine-readable citation metadata is available in CITATION.cff.

Copyright and licensing

Copyright and attribution notices in the source files and imported libraries remain applicable. This repository has no single project-wide license grant; consult the relevant notices and rights holders before redistribution or reuse. The paper figure retains its original attribution, documented in the image source record.