The readings shared in Bluesky on 18 July 2025 are

• Teaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. #CompSci #Teaching #ITP #LeanProver #ACL2
• CSLib: An open-source Lean 4 library formalizing a significant subsetof undergraduate-level computer science. ~ Clark Barrett et als. #ITP #LeanProver #CompSci
• Quantifiers for differentiable logics in Rocq (Extended abstract). ~ Jairo Miguel Marulanda-Giraldo et als. #ITP #Rocq
• Comparing codes: Binary search in a 2D matrix. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. ~ Xingguang Ji et als. #LLMs #ITP #LeanProver