#cslib — Public Fediverse posts

🎉 CSLib now includes a fully verified proof of the famous FLP (Fischer, Lynch and Paterson) result: it is impossible to achieve consensus in a distributed system with a faulty process and asynchronous messaging.

Great work by Ching-Tsun Chou, which formalises the constructive pen & paper proof by Hagen Völzer in 2004.

1/2

#CSLib #FormalMethods #Lean #FORM

🎉 CSLib now includes a fully verified proof of the famous FLP (Fischer, Lynch and Paterson) result: it is impossible to achieve consensus in a distributed system with a faulty process and asynchronous messaging.

Great work by Ching-Tsun Chou, which formalises the constructive pen & paper proof by Hagen Völzer in 2004.

1/2

#CSLib #FormalMethods #Lean #FORM

🌐 You can now play with CSLib directly in your browser at https://live.lean-lang.org/! Many thanks to Robert Simmons for this! 👏

#Lean #CSLib #FormalMethods

🌐 You can now play with CSLib directly in your browser at https://live.lean-lang.org/! Many thanks to Robert Simmons for this! 👏

#Lean #CSLib #FormalMethods

📣 Job alert: we're hiring PhDs and postdocs at FORM! Come work with us on formal methods, programming, verification, Lean, and #CSLib. We have many possible projects or you can propose your own.

Deadline for applications: 16 August 2026

Links to the calls below.

PhD call: https://fa-eosd-saasfaprod1.fa.ocs.oraclecloud.com/hcmUI/CandidateExperience/da/sites/CX_1001/job/4058/?utm_medium=jobshare&utm_source=External+Job+Share
Postdoc call: https://fa-eosd-saasfaprod1.fa.ocs.oraclecloud.com/hcmUI/CandidateExperience/da/sites/CX_1001/job/4076/?utm_medium=jobshare&utm_source=External+Job+Share

📣 Job alert: we're hiring PhDs and postdocs at FORM! Come work with us on formal methods, programming, verification, Lean, and #CSLib. We have many possible projects or you can propose your own.

Deadline for applications: 16 August 2026

Links to the calls below.

PhD call: https://fa-eosd-saasfaprod1.fa.ocs.oraclecloud.com/hcmUI/CandidateExperience/da/sites/CX_1001/job/4058/?utm_medium=jobshare&utm_source=External+Job+Share
Postdoc call: https://fa-eosd-saasfaprod1.fa.ocs.oraclecloud.com/hcmUI/CandidateExperience/da/sites/CX_1001/job/4076/?utm_medium=jobshare&utm_source=External+Job+Share

You can always check the team curating CSLib at https://github.com/leanprover/cslib/blob/main/GOVERNANCE.md, which we keep up to date.

#Lean #CSLib #OpenSource

2/2

You can always check the team curating CSLib at https://github.com/leanprover/cslib/blob/main/GOVERNANCE.md, which we keep up to date.

#Lean #CSLib #OpenSource

2/2

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

Thanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.

#CSLib #AI #Lean #FORM #FormalMethods

3/3

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.

#Lean #FormalMethods #CSLib #FORM

2/2

We offer a library-level solution in #CSLib through the 'HasFresh' typeclass. Whatever the type of x is, you just need to convince #Lean that there's a 'fresh' value generator and you're good to go with your proofs. For many types (like natural numbers), we've even already convinced Lean for you.

This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.

2/

We offer a library-level solution in #CSLib through the 'HasFresh' typeclass. Whatever the type of x is, you just need to convince #Lean that there's a 'fresh' value generator and you're good to go with your proofs. For many types (like natural numbers), we've even already convinced Lean for you.

This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.

2/

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. https://arxiv.org/abs/2602.15078v1 #LeanProver #ITP #CSLib #CompSci

Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. https://arxiv.org/abs/2602.15078v1 #LeanProver #ITP #CSLib #CompSci

Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. https://arxiv.org/abs/2602.15409v1 #LeanProver #ITP #CSLib #CompSci

Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. https://arxiv.org/abs/2602.15409v1 #LeanProver #ITP #CSLib #CompSci

RE: https://mastodon.acm.org/@acp/115921453909423834

The recording for @fmontesi's Lean Together talk, "CSLib: The Lean Computer Science Library", is now online:

https://www.youtube.com/watch?v=KfIZn2zH8CA

#CSLib #LeanProver

@fmontesi is presenting the first results and next steps of CSLib – the Lean Computer Science library – at Lean Together tomorrow (20 Jan) at 14:00 CET. The event is online and open to all, so feel free to join if you're curious:

https://researchseminars.org/talk/LT2026/9/

@leanprover #CSLib #LeanProver

FORM (https://sdu.dk/form) is a new research centre at the University of Southern Denmark. It is a major investment in formalised computer science and reliable AI-assisted programming. We collaborate heavily with the #Lean FRO and other international partners on #CSLib.

FORM (https://sdu.dk/form) is a new research centre at the University of Southern Denmark. It is a major investment in formalised computer science and reliable AI-assisted programming. We collaborate heavily with the #Lean FRO and other international partners on #CSLib.

~ Academic Positions in Formal Methods (postdoc, assistant prof., associate prof.) and Programming Languages (postdoc) ~

The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! Among other projects, FORM is also working on the formalisation of computer science as part of a global initiative, CSLib, in @leanprover.

(1/3)

#formalMethods #LeanProver #typeTheory #programmingLanguages #academicJobs #fediHire #FORMSDU #SDUDK #CSLib

@fmontesi will be the first director of the new Centre for Formal Methods and Future Computing (FORM) here at the University of Southern Denmark!

Among other things, the Centre will work on the development of @leanprover's CS Library, where Fabrizio already serves as a member of the steering committee.

Interested in research in formal methods? Please expect job announcements very soon.

https://sdu.dk/form

#formalMethods #LeanProver #CSLib #programmingLanguages #FORMSDU #SDUDK