🎓 PhD Positions in Computer Science (Formal Methods) 🇩🇰 | University of Southern Denmark 📌 Position: PhD in Computer Science (Formal Methods) 🏫 University: University of Southern Denmark (SDU) 📍 Location: Odense / Vejle, Denmark 🇩🇰 🏢 Department: Mathematics & Computer Science 👨‍🏫 Supervisor: Fabrizio Montesi 📅 Deadline: August 16, 2026 ⏳ Duration: 3 years (fully funded) 🔬 About the Project The Centre for Formal Methods and Future Computing (FORM) invites applications for PhD positions focused on advancing the formalisation of computing. The research aims to combine human intelligence and AI to build reliable digital systems grounded in rigorous mathematical foundations. Key research areas include: • Computational complexity • Distributed systems & cloud computing • Logic and theorem proving • Programming languages & type systems • Security, cryptography & privacy • Human factors in computing A major initiative includes contributing to the Computer Science Library (CSLib) using Lean, a global effort to formalise computer science knowledge. 👤 Ideal Candidate • Master’s degree in Computer Science or related field • Strong interest in formal methods (theory or applications) • Solid analytical and programming skills • Ability to work in an international research environment • Fluency in English 🌟 Why Apply? • Join a leading research centre in formal methods and AI • Work on foundational challenges in computing and software reliability • Collaborate within a strong interdisciplinary research cluster (AI, cybersecurity, programming languages) • Access to international collaborations and global initiatives • Supportive and inclusive academic environment 🌍 Location Highlight – Odense Odense, Denmark’s third-largest city, offers a high quality of life with a mix of historic charm and modern living. Located on the island of Funen, it provides easy access to Copenhagen and Aarhus, along with beautiful coastal areas. 🔗 More Info: phdscanner.com/opportunities… #PhD #ComputerScience #FormalMethods #ProgrammingLanguages #DistributedSystems #Cybersecurity #Denmark #ResearchOpportunity #AcademicJobs #PhDPositions

I'm looking for a postdoc to work on Separation Logic in Lean. Position in the London Meta office, in the new AI Verification team. Possibly collaborating with or building on external work on CSLib, Iris-Lean and loom.@AIatMeta @leanprover metacareers.com/profile/job_…

CSLib has a monad that "counts" resources (time or memory) that you can prove a bound on. Figures 3 and 4 of arxiv.org/pdf/2602.04846 have some examples. Caveat 1: you need to manually label statements to count. Caveat 2: I suspect it's not possible to do both mem/time together.

Leonardo de Moura: Machine-Checked Mathematics in the Age of AI youtu.be/objFfoJRH_U. Clark Barrett: CSLib - Building a Platform for AI-assisted Formal Verification in Lean youtu.be/txRvy9hv52M. Michael Freedman: Compression Is All You Need - Modeling Mathematics youtu.be/4nM82nZzIxU. Kevin Buzzard: On Autoformalisation youtu.be/etZzn1Q7is0. Andrea Bertozzi: A foray into AI for Mathematics youtu.be/bx4BfuVFaPg. Adam Brown: A.G.I. and the Future of Reasoning youtu.be/gf1uwCH0HUU. Deirdre Haskell: Mathematical AI at the Fields Institute youtu.be/8lcHpsuIsOM.

Interested in formal methods and AI? Submit a talk/poster proposal for our CAV 2026 workshop on AI for Math and Computer Science Research (AIMACS)! sites.google.com/d/1DiW7HZSk…. Talks/posters must be based on work publicly released in the last year and submitted through this form: forms.gle/RESRT5uXXtZkVzjr9. The submission deadline is May 31. The workshop is in Lisbon on July 25. Other program highlights include a tutorial on Lean CSLib and invited talks on AI-aided theorem-proving and algorithm discovery.

What if we could mathematically prove that code does what it's supposed to do, not just test it and hope? The Caltech AI Alignment Group hosted @ClarkBarrett7 from @Stanford for a talk on CSLib, a platform for AI-assisted formal verification in Lean, and why proving code correct is becoming one of the most urgent problems in AI safety. 1/7

CLBO (CsLiB₆O₁₀) 非線形光学結晶。LBOとCBOの混晶っぽいですが構造はこれらとは異なります。180nmまで透明でYAGの第４・第５高調波の発振に適しており、BBOよりも高効率な発振が可能です。CLBOが組み込まれた紫外固体レーザが販売されています。

少し形式化から離れてふと戻ってきたらcslibに様相論理が生えてきて「おもしろいことしてんねー＾＾アタイも少し混ぜてよ～ー」という感じになったので、連絡した

There's a lot of low-hanging fruit in CSlib for Indian students to contribute to, such as Boole - a new intermediate verification language to help with reasoning about traditional code (Python, Rust etc) inside Lean. CSlib at present is similar to how mathlib used to be 7 years ago. cslib.io/

Lean is fun. Really. And I've got the real challenge for the next months until I find a new full time employment: reimplementing the whole cryptographic stack of Mina, in Lean... Why? First, it is a very challenging work. Totally aligned with my current interests, and with what I know. And I need to have my brain working! (I feel I'm getting dumb!) Second: it's a full stack work. It goes to vanilla PlonK, define the snarky DSL, define custom gates, lookup protocols (with the fancy runtime lookups, never specified), but also... Recursion using Halo. Which would be fun for other projects like Zcash, Midnight, etc. An important note is that Pickles, the recursive layer of Mina, was actually already built with formal verification in mind. When you look at the code, you've got some encoded theories to encode invariants. It would pursue Izaak initial vision - I guess that was the vision. It will also include the Pasta curves, Poseidon, Schnorr signatures, etc. Maybe multisignatute using FROST. Third, it will also force me to go deeper into the theory and the papers, and it will probably useful to contribute to ArkLib and CSLib at the same time. Long term wish for me. I guess the whole codebase will be compilable into C directly, and we could optimize later the generated code to have a more efficient implementation, and have bindings that could be used on production by an actual Mina node. When this is done, the blockchcain and the transaction snark could be reimplemented on top. And I could finally implement the standard signature schemes... And nothing will be vibe coded. I'm done with this. Let's have fun!

@miike reminded me that the GSAI summit was also a key catalyst for Lean's #cslib (cslib.io)!

🚀 CSLib is Growing 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). @leanprover (1/2)

Now that formalization is so feasible, one-shotting textbooks and papers seems low value to me unless we’re concerned with the validity of the results. Results should be formalized in context of usable theory and in a way that makes for good and maintainable software (eg mathlib, cslib, arklib, etc)

Oh, I just noticed you're a maintainer of cslib! I was talking with @swarat last year as it was just coming together. How would you say it's progressing?

Lean側としては汎用言語としての側面を売り出したいみたいだけど、LLMの登場も相まって数学的用途ばっか着目されてる感はあるよね。 CSLibが発展してプログラムの形式検証がやりやすくなればワンチャンあるだろうか、って見立て

We’re excited to release TorchLean which is the first fully verified neural network framework in Lean. The Lean community has largely focused on pure mathematics. TorchLean expands this frontier toward verified neural network software and scientific computing. With the recent release of CSlib, we see this as another step toward a fully verified ML stack. We support features: 1. Executable IEEE-754 floating-point semantics (and extensible alternative FP models) verified tensor abstractions with precise shape/indexing semantics 2. Formally verified autograd system for differentiation of NN programs Proof-checked certification / verification algorithms like CROWN (robustness, bounds, etc.) 3. PyTorch-inspired modeling API with eager-style development export/lowering to a shared IR for execution and verification Project page: leandojo.org/torchlean.html Paper: [2602.22631] TorchLean: Formalizing Neural Networks in Lean Work done @Robertljg, Jennifer Cruden, Xiangru Zhong, @huan_zhang12 and @AnimaAnandkumar. #MachineLearning #ScientificComputing #Lean

計算機科学版 MathLib の CSLib ちょっとずつ触って遊び始めました。 面白そうなネタができたらそのうち記事書きます。 cslib.io/

Came across CSLib, a formal verification library for CS foundations. The goal is to formalize everything under the sun in computer science starting from simple algorithms, to lambda-calculus to distributed system protocols. They’ve created a new Intermediate Verification Language (IVL) called Boole. The goal isn't just to write Lean; it's to transpile Rust, C , and Python into Boole, generate "Verification Conditions" in Lean, and use solvers (SMT/AI) to prove them. By using pre-verified CSLib components, it can help to build large-scale systems without reinventing the wheel for every proof. It also serves a dual purpose: it provides high-quality training data for AI provers (like AlphaProof), and those same AI tools will eventually help humans write CSLib proofs faster. cslib.io/ arxiv.org/pdf/2602.04846

An interesting angle that lines up with some of my intuitions: - the influence of Mathlib on Lean benchmarks - qualitative differences between CS/math that affect AI formalization I hope in the future this can consider CSLib, which occupies an interesting space wrt these points.

We've thought about this in CSLib and tried for instance to use metaprogramming to connect things a bit more broadly than is practical at the object level, but this is all pretty early work. There's some discussion of this in: arxiv.org/abs/2602.15078