Repositories list

• SECOMP

  Public
  SECOMP formally secure compiler for compartmentalized C programs (based on CompCert)

  Rocq Prover

  •

  Other

  •260260 forks•1212 stars•66 issues•22 pull requests•Updated Jun 16, 2026Jun 16, 2026

• Triosecuris

  Public
  Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking

  Rocq Prover

  •11 fork•33 stars•00 issues•00 pull requests•Updated Apr 14, 2026Apr 14, 2026

• exploring-robust-property-preservation

  Public
  Coq development for "Journey Beyond Full Abstraction" paper

  Rocq Prover

  •

  Apache License 2.0

  •00 forks•88 stars•00 issues•00 pull requests•Updated Mar 22, 2026Mar 22, 2026

• secure-compilation.github.io

  Public
  Code for SECOMP project website: https://secure-compilation.github.io

  HTML

  •00 forks•11 star•00 issues•00 pull requests•Updated Dec 13, 2025Dec 13, 2025

• nanopass-bt

  Public
  Rocq development for the paper Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

  Rocq Prover

  •00 forks•00 stars•00 issues•00 pull requests•Updated Sep 22, 2025Sep 22, 2025

• comparing_speculative_semantics_rocq

  Public
  Rocq Prover

  •00 forks•00 stars•00 issues•00 pull requests•Updated Aug 21, 2025Aug 21, 2025

• when-good-components-go-bad

  Public
  Coq formalization for "When Good Components Go Bad" paper, with various later extensions

  coqundefined-behaviorcompartmentalization+ 3

  coqundefined-behaviorcompartmentalizationsecure-compilationtagged-architecturessoftware-fault-isolation

  Coq

  •

  Apache License 2.0

  •11 fork•88 stars•11 issue•11 pull request•Updated Aug 11, 2025Aug 11, 2025

• fslh-rocq

  Public
  FSLH: Flexible Mechanized Speculative Load Hardening

  Coq

  •00 forks•33 stars•00 issues•00 pull requests•Updated May 16, 2025May 16, 2025

• different_traces

  Public
  The Coq development for "Trace-Relating Compiler Correctness and Secure Compilation" paper

  Coq

  •

  Apache License 2.0

  •00 forks•22 stars•00 issues•00 pull requests•Updated May 8, 2025May 8, 2025

• SecurePtrs

  Public
  Coq formalization for "SecurePtrs" paper

  coqcapabilitiescompartmentalization+ 1

  coqcapabilitiescompartmentalizationsecure-compilation

  Coq

  •

  Apache License 2.0

  •00 forks•33 stars•00 issues•00 pull requests•Updated Jun 3, 2022Jun 3, 2022

• ds-2018

  Public
  Materials of Dagstuhl Seminar 18201 on Secure Compilation (May 13-18, 2018)

  00 forks•00 stars•00 issues•00 pull requests•Updated Nov 9, 2018Nov 9, 2018

• beyond-good-and-evil

  Public
  Auxiliary materials for "Beyond Good and Evil" paper

  Coq

  •

  Apache License 2.0

  •00 forks•33 stars•22 issues•00 pull requests•Updated Feb 16, 2018Feb 16, 2018