Logic and Semantics @ Aarhus University

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

logsem/clutch’s past year of commit activity

Rocq Prover
35
MIT
9 0 2
Updated Mar 5, 2026
griotte Public
Rocq implementation of Griotte

logsem/griotte’s past year of commit activity

Rocq Prover
2
0
0 3
Updated Mar 4, 2026
logsem/iris-project’s past year of commit activity

HTML
2 26 1 2
Updated Feb 26, 2026
aneris Public
Program logic for developing and verifying distributed systems

logsem/aneris’s past year of commit activity

Rocq Prover
36
MIT
8 4 0
Updated Feb 25, 2026
trillium Public
The Trillium logic for proving trace refinement properties such as liveness via Iris

logsem/trillium’s past year of commit activity

Coq
4
MIT
3 0 4
Updated Feb 13, 2026
AxSL Public
AxSL, a concurrent separation logic for Arm's relaxed concurrency

logsem/AxSL’s past year of commit activity

Rocq Prover
1 1 0 0
Updated Jan 21, 2026
iris-wasmfx Public
Iris-WasmFX program logic and logical relation for WasmFX

logsem/iris-wasmfx’s past year of commit activity

Rocq Prover
4
MIT 0
0 0
Updated Dec 6, 2025
cerisier Public
Formalisation in Rocq of CHERI-TrEE

logsem/cerisier’s past year of commit activity

Rocq Prover
2
0
0 0
Updated Nov 11, 2025
logsem/spirea’s past year of commit activity

Coq
3 1 0 0
Updated Oct 20, 2025
logsem/machine_utils’s past year of commit activity

Coq
1
0
0 0
Updated Sep 21, 2025