| Website | https://www.fabriziomontesi.com/ |
| Choreographic Programming | https://en.wikipedia.org/wiki/Choreographic_programming |
| Jolie Language | https://en.wikipedia.org/wiki/Jolie_(programming_language) |
| YouTube | https://youtube.com/@fmontesi |
'Pact: A Choreographic Language for Agentic Ecosystems' develops a choreographic language extended with operations to describe agent choices and preferences, capturing important LLM interaction scenarios. Very nice! By Kiran Gopinathan, Jack Feser, Michelangelo Naim, Zenna Tavares, and Eli Bingham. (Picture from the talk in the first link.)
Learn more: https://www.basis.ai/blog/choreographies/
Paper: https://arxiv.org/abs/2605.03143
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
We then entered a fascinating group discussion on how to move AI and software development forward – providing robust frameworks, languages, and knowledge bases for AI to grow well, so that it can carry out sophisticated coding and even contribute to computer science research. All with the crucial aspect of providing verifiable proofs in mind, of course!
2/
Artificial Intelligence 🤝 Formal Methods
Last week we had a very interesting online workshop with people from Mistral AI and FORM. First we had two seminars: Albert Jiang presented their latest work at Mistral for verifiable AI-generated math in Lean, and I presented the vision and codebase of CSLib (the Lean Computer Science Library).
1/
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
👥 Save the date: CSLib Online Meetings
Announcing the beginning of the CSLib online meetings, aimed at coordinating and facilitating the development of the library and its use. The meetings are an opportunity to discuss CSLib and exchange information with the rest of the community and the maintainers.
The first meeting will take place on Thursday, 21 May 2026, at 12:30.
1/
Generality brings further utility. Based on HasFresh, CSLib's free_union tactic will automatically look at your context for you and try to collect all current values into a finite set. You can then use HasFresh's API to get a fresh value that is different from all those in your context.
Just like on pen and paper: pick a fresh x!
Check out HasFresh at https://api.cslib.io/docs/Cslib/Foundations/Data/HasFresh.html
3/3
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/
🔦 CSLib feature spotlight: fresh values. A great example of theory meeting practice.
In many explanations of programs and proofs in computer science, you might find sentences like:
- 'Pick a fresh value x not in the set'
- 'For a fresh x'
- 'Where x is a fresh name not in the program P'
etc.
I myself must've seen this pattern hundreds of times in compilers, process models, and semantics – to mention a few.
1/
🚀 CSLib is Growing – Follow Its Journey!
The #Lean Computer Science Library (#CSLib) – a global effort to build reusable infrastructure for formal methods in AI-ready computer programming and research – is gaining momentum (> 100 forks, > 400 PRs, and nearly 500 stars on GitHub).
If you’re curious about its progress, the contributions we seek, or the open challenges we’re discussing, watch this space. I’ll start sharing updates about these topics soon.
