compcert
Here are 11 public repositories matching this topic...
Verified Software Toolchain
-
Updated
Sep 3, 2026 - Rocq Prover
A Lustre compiler in Coq
-
Updated
Aug 28, 2026 - Rocq Prover
A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
-
Updated
Jul 21, 2026 - Rocq Prover
Towards a verified back-end for The Glorious Glasgow Haskell Compilation System
-
Updated
Aug 26, 2026 - Rocq Prover
Docker images of the Coq proof assistant with compcert and VST pre-installed
-
Updated
Feb 15, 2022 - Shell
Formally verified 63-bit integer arithmetic, implemented in C and proven in Coq
-
Updated
Mar 4, 2022 - Coq
PSL: A Paninian type system for verifiable embedded firmware. 15 proof sprints, 206 machine-checked assertions, Lean 4 formal semantics. Structural inexpressibility of embedded bugs.
-
Updated
Jul 10, 2026 - Python
Tools for working with Verified Software Units
-
Updated
Jan 19, 2022 - OCaml
This repository contains the mCertiKOS certified operating system kernel, focusing on security and formal verification using Coq and CompCert. It supports building and testing on bare-metal or QEMU environments.
-
Updated
Jan 3, 2025 - Coq
Verified finite state automata compiler
-
Updated
Aug 10, 2026 - Rocq Prover
Add this topic to your repo
To associate your repository with the compcert topic, visit your repo's landing page and select "manage topics."