This is an unofficial reimagining of the Archive of Formal Proofs
Hybrid Multi-Lane Spatial Logicby Sven Linker