Repositories list

• clutch

  Public
  Probabilistic separation logics for verifying higher-order probabilistic programs.

  asynchronouscoqlogic+ 6

  asynchronouscoqlogicirisprobabilisticrelationalhigher-orderseparation-logiccouplings

  Rocq Prover

  •

  MIT License

  •1111 forks in logsem/clutch•4646 stars in logsem/clutch•00 issues in logsem/clutch•44 pull requests in logsem/clutch•Updated Nov 11, 2026Nov 11, 2026

• griotte

  Public
  Rocq implementation of Griotte

  Rocq Prover

  •

  Other

  •00 forks in logsem/griotte•22 stars in logsem/griotte•00 issues in logsem/griotte•11 pull request in logsem/griotte•Updated Nov 7, 2026Nov 7, 2026

• clutch-lean

  Public
  Probabilistic separation logics for verifying higher-order probabilistic programs in Lean.

  Lean

  •00 forks in logsem/clutch-lean•22 stars in logsem/clutch-lean•00 issues in logsem/clutch-lean•00 pull requests in logsem/clutch-lean•Updated Nov 6, 2026Nov 6, 2026

• cerise

  Public
  Formalisation of a capability machine and principles for reasoning about security properties

  Rocq Prover

  •

  Other

  •88 forks in logsem/cerise•2929 stars in logsem/cerise•55 issues in logsem/cerise•22 pull requests in logsem/cerise•Updated Oct 13, 2026Oct 13, 2026

• iris-project

  Public
  HTML

  •3030 forks in logsem/iris-project•33 stars in logsem/iris-project•11 issue in logsem/iris-project•22 pull requests in logsem/iris-project•Updated Oct 4, 2026Oct 4, 2026

• iris-lecture-notes

  Public
  TeX

  •

  Other

  •66 forks in logsem/iris-lecture-notes•1919 stars in logsem/iris-lecture-notes•1010 issues in logsem/iris-lecture-notes•00 pull requests in logsem/iris-lecture-notes•Updated Sep 26, 2026Sep 26, 2026

• iris-tutorial-lean

  Public
  Iris tutorial in Lean

  Lean

  •

  Other

  •33 forks in logsem/iris-tutorial-lean•33 stars in logsem/iris-tutorial-lean•00 issues in logsem/iris-tutorial-lean•11 pull request in logsem/iris-tutorial-lean•Updated Sep 5, 2026Sep 5, 2026

• cerise-interpreter

  Public
  OCaml

  •

  Other

  •00 forks in logsem/cerise-interpreter•33 stars in logsem/cerise-interpreter•00 issues in logsem/cerise-interpreter•00 pull requests in logsem/cerise-interpreter•Updated Aug 31, 2026Aug 31, 2026

• lawyer

  Public
  Rocq mechanization of Lawyer liveness logic and its extension for wait-freedom

  Rocq Prover

  •

  MIT License

  •00 forks in logsem/lawyer•33 stars in logsem/lawyer•00 issues in logsem/lawyer•00 pull requests in logsem/lawyer•Updated Aug 26, 2026Aug 26, 2026

• trillium

  Public
  The Trillium logic for proving trace refinement properties such as liveness via Iris

  Coq

  •

  MIT License

  •33 forks in logsem/trillium•77 stars in logsem/trillium•00 issues in logsem/trillium•44 pull requests in logsem/trillium•Updated Aug 26, 2026Aug 26, 2026

• iris-tutorial

  Public
  Rocq Prover

  •

  MIT License

  •4646 forks in logsem/iris-tutorial•109109 stars in logsem/iris-tutorial•00 issues in logsem/iris-tutorial•00 pull requests in logsem/iris-tutorial•Updated Jul 31, 2026Jul 31, 2026

• spirea

  Public
  Coq

  •11 fork in logsem/spirea•55 stars in logsem/spirea•00 issues in logsem/spirea•00 pull requests in logsem/spirea•Updated Jul 7, 2026Jul 7, 2026

• gitrees

  Public
  guarded interaction trees

  Rocq Prover

  •33 forks in logsem/gitrees•1414 stars in logsem/gitrees•00 issues in logsem/gitrees•22 pull requests in logsem/gitrees•Updated Jul 6, 2026Jul 6, 2026

• aneris

  Public
  Program logic for developing and verifying distributed systems

  distributed-systemscoqiris+ 1

  distributed-systemscoqirisseparation-logic

  Rocq Prover

  •

  MIT License

  •88 forks in logsem/aneris•3939 stars in logsem/aneris•44 issues in logsem/aneris•00 pull requests in logsem/aneris•Updated Apr 29, 2026Apr 29, 2026

• cerisier

  Public
  Formalisation in Rocq of CHERI-TrEE

  Rocq Prover

  •

  Other

  •00 forks in logsem/cerisier•22 stars in logsem/cerisier•00 issues in logsem/cerisier•00 pull requests in logsem/cerisier•Updated Apr 8, 2026Apr 8, 2026

• iris-nextgen

  Public
  Next generation modality for Iris

  Coq

  •22 forks in logsem/iris-nextgen•44 stars in logsem/iris-nextgen•00 issues in logsem/iris-nextgen•00 pull requests in logsem/iris-nextgen•Updated Apr 7, 2026Apr 7, 2026

• adiar

  Public
  External Memory (Binary) Decision Diagrams

  bddbinary-decision-diagramsexternal-memory+ 2

  bddbinary-decision-diagramsexternal-memoryzddzero-suppressed-decision-diagrams

  C++

  •

  MIT License

  •1616 forks in logsem/adiar•00 stars in logsem/adiar•00 issues in logsem/adiar•00 pull requests in logsem/adiar•Updated Mar 24, 2026Mar 24, 2026

• machine_utils

  Public
  Coq

  •00 forks in logsem/machine_utils•11 star in logsem/machine_utils•00 issues in logsem/machine_utils•00 pull requests in logsem/machine_utils•Updated Mar 20, 2026Mar 20, 2026

• iris-wasmfx

  Public
  Iris-WasmFX program logic and logical relation for WasmFX

  Rocq Prover

  •

  MIT License

  •00 forks in logsem/iris-wasmfx•44 stars in logsem/iris-wasmfx•00 issues in logsem/iris-wasmfx•00 pull requests in logsem/iris-wasmfx•Updated Mar 15, 2026Mar 15, 2026

• AxSL

  Public
  AxSL, a concurrent separation logic for Arm's relaxed concurrency

  armconcurrencyverification+ 1

  armconcurrencyverificationseparation-logic

  Rocq Prover

  •

  Other

  •11 fork in logsem/AxSL•11 star in logsem/AxSL•00 issues in logsem/AxSL•00 pull requests in logsem/AxSL•Updated Jan 21, 2026Jan 21, 2026

• synthetic_domains

  Public
  Coq

  •

  MIT License

  •00 forks in logsem/synthetic_domains•22 stars in logsem/synthetic_domains•00 issues in logsem/synthetic_domains•00 pull requests in logsem/synthetic_domains•Updated May 14, 2025May 14, 2025

• iriswasm

  Public
  IrisWasm program logic and logical relation for WebAssembly

  Coq

  •

  MIT License

  •00 forks in logsem/iriswasm•44 stars in logsem/iriswasm•00 issues in logsem/iriswasm•00 pull requests in logsem/iriswasm•Updated May 2, 2025May 2, 2025

• melocoton

  Public
  Coq

  •

  Other

  •11 fork in logsem/melocoton•1313 stars in logsem/melocoton•55 issues in logsem/melocoton•00 pull requests in logsem/melocoton•Updated Apr 28, 2025Apr 28, 2025

• MSWasm

  Public
  Coq

  •

  MIT License

  •00 forks in logsem/MSWasm•44 stars in logsem/MSWasm•00 issues in logsem/MSWasm•00 pull requests in logsem/MSWasm•Updated Aug 19, 2024Aug 19, 2024

• fw-rec-inj

  Public
  Coq

  •

  MIT License

  •00 forks in logsem/fw-rec-inj•22 stars in logsem/fw-rec-inj•11 issue in logsem/fw-rec-inj•11 pull request in logsem/fw-rec-inj•Updated Mar 11, 2024Mar 11, 2024

• well-bracketed-logic

  Public
  Coq

  •

  MIT License

  •00 forks in logsem/well-bracketed-logic•33 stars in logsem/well-bracketed-logic•00 issues in logsem/well-bracketed-logic•00 pull requests in logsem/well-bracketed-logic•Updated Jan 2, 2024Jan 2, 2024

• machine_program_logic

  Public
  Coq

  •00 forks in logsem/machine_program_logic•00 stars in logsem/machine_program_logic•00 issues in logsem/machine_program_logic•00 pull requests in logsem/machine_program_logic•Updated Dec 14, 2023Dec 14, 2023

• terpsichore

  Public
  Studying and Formalising Choreographies in Iris

  00 forks in logsem/terpsichore•00 stars in logsem/terpsichore•00 issues in logsem/terpsichore•00 pull requests in logsem/terpsichore•Updated Oct 31, 2023Oct 31, 2023

• two_pcf_models

  Public
  Two models of PCF in siProp

  Coq

  •00 forks in logsem/two_pcf_models•00 stars in logsem/two_pcf_models•00 issues in logsem/two_pcf_models•00 pull requests in logsem/two_pcf_models•Updated Jul 14, 2023Jul 14, 2023

• mitten_preorder

  Public
  OCaml

  •

  MIT License

  •22 forks in logsem/mitten_preorder•3434 stars in logsem/mitten_preorder•11 issue in logsem/mitten_preorder•00 pull requests in logsem/mitten_preorder•Updated Apr 17, 2023Apr 17, 2023