# Jobs

**URL:** https://discourse.rocq-prover.org/c/announcements/jobs/26.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [About the Jobs category](https://discourse.rocq-prover.org/t/about-the-jobs-category/2824)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [September 9, 2025, 3:03pm UTC](https://discourse.rocq-prover.org/t/about-the-jobs-category/2824 "2025-09-09T15:03:28Z")

</div>

This sub-category can be used for job postings. Jobs may also be posted in categories Announcements, \[de\] Rocq auf Deutsch \> Ankündigungen, \[es\] ¡Rocq en español! \> Anuncios, \[fr\] Rocq en français \> Annonces, \[ru\] Rocq н…

---

## [PhD position at TU Delft: deriving formal languages from their semantics](https://discourse.rocq-prover.org/t/phd-position-at-tu-delft-deriving-formal-languages-from-their-semantics/3146)

<div class="topic-metadata">

**Author:** [@benediktahrens](https://discourse.rocq-prover.org/u/benediktahrens)\
**Replies:** 0\
**Last updated:** [October 16, 2026, 10:02am UTC](https://discourse.rocq-prover.org/t/phd-position-at-tu-delft-deriving-formal-languages-from-their-semantics/3146 "2026-10-16T10:02:34Z")

</div>

PhD position at TU Delft: deriving formal languages from their semantics I am looking for a PhD candidate for a 4-year position in the Department of Software Technology at TU Delft, funded by the Air Force Office of Sci…

---

## [Research roles at Melbourne on seL4, agentic security, neural theorem proving](https://discourse.rocq-prover.org/t/research-roles-at-melbourne-on-sel4-agentic-security-neural-theorem-proving/3127)

<div class="topic-metadata">

**Author:** [@toby.murray](https://discourse.rocq-prover.org/u/toby.murray)\
**Replies:** 0\
**Last updated:** [October 5, 2026, 4:50am UTC](https://discourse.rocq-prover.org/t/research-roles-at-melbourne-on-sel4-agentic-security-neural-theorem-proving/3127 "2026-10-05T04:50:00Z")

</div>

Research positions in seL4, formal verification and AI-assisted theorem proving for agentic security at the University of Melbourne The University of Melbourne is recruiting Postdoctoral Research Fellows / Research Fell…

---

## [Chaire de Professeur Junior in Lyon: Generative AI for formal proofs](https://discourse.rocq-prover.org/t/chaire-de-professeur-junior-in-lyon-generative-ai-for-formal-proofs/3094)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [August 27, 2026, 10:15am UTC](https://discourse.rocq-prover.org/t/chaire-de-professeur-junior-in-lyon-generative-ai-for-formal-proofs/3094 "2026-08-27T10:15:47Z")

</div>

The CNRS (French National Centre for Scientific Research) opens a CPJ (= Chaire de Professeur Junior) this year on the topic “Generative AI for formal proofs”. This is a tenure-track position. After 3 to 6 years, the …

---

## [MITACS Undergrad Research Internships - 2027 Applications Open](https://discourse.rocq-prover.org/t/mitacs-undergrad-research-internships-2027-applications-open/3080)

<div class="topic-metadata">

**Author:** [@JoeyEremondi](https://discourse.rocq-prover.org/u/JoeyEremondi)\
**Replies:** 0\
**Last updated:** [August 7, 2026, 4:02pm UTC](https://discourse.rocq-prover.org/t/mitacs-undergrad-research-internships-2027-applications-open/3080 "2026-08-07T16:02:57Z")

</div>

The MITACS GlobalLink program allows undergraduate students from across the world to complete paid research internships at Canadian universities. The internships last 12 weeks, with start dates between May 1 and July 31. …

---

## [Blockchain formal verification @ category labs](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043)

<div class="topic-metadata">

**Author:** [@aa755](https://discourse.rocq-prover.org/u/aa755)\
**Replies:** 0\
**Last updated:** [June 6, 2026, 12:01am UTC](https://discourse.rocq-prover.org/t/blockchain-formal-verification-category-labs/3043 "2026-06-06T00:01:16Z")

</div>

Monad is like Ethereum but aims to be faster using higher parallelism/pipelining across the entire stack. We use iris and BRiCk C++ semantics to formally verify monad’s C++ implementation. A blog post explaining our ver…

---

## [Permanent researcher position at Mines Paris - PSL](https://discourse.rocq-prover.org/t/permanent-researcher-position-at-mines-paris-psl/3036)

<div class="topic-metadata">

**Author:** [@olivhash](https://discourse.rocq-prover.org/u/olivhash)\
**Replies:** 0\
**Last updated:** [May 29, 2026, 9:45am UTC](https://discourse.rocq-prover.org/t/permanent-researcher-position-at-mines-paris-psl/3036 "2026-05-29T09:45:19Z")

</div>

The Computer Science research center at Mines Paris - PSL is hiring a permanent researcher in the domain of compilation, HPC, code efficiency, or formal verification. The job offer is written in French, but anybody (w…

---

## [Technical Associate positoin at the AI for Math Fund](https://discourse.rocq-prover.org/t/technical-associate-positoin-at-the-ai-for-math-fund/3035)

<div class="topic-metadata">

**Author:** [@faenuccio](https://discourse.rocq-prover.org/u/faenuccio)\
**Replies:** 0\
**Last updated:** [May 29, 2026, 1:28am UTC](https://discourse.rocq-prover.org/t/technical-associate-positoin-at-the-ai-for-math-fund/3035 "2026-05-29T01:28:46Z")

</div>

Double-positing here: Hi all, The AI for Math Fund Team at Renaissance Philanthropy is hiring a Technical Associate. We’re interested in candidates with strong mathematical and technical backgrounds in the AI for Math…

---

## [Permanent lecturer position at the University of Strathclyde](https://discourse.rocq-prover.org/t/permanent-lecturer-position-at-the-university-of-strathclyde/2966)

<div class="topic-metadata">

**Author:** [@gallais](https://discourse.rocq-prover.org/u/gallais)\
**Replies:** 0\
**Last updated:** [March 9, 2026, 1:30pm UTC](https://discourse.rocq-prover.org/t/permanent-lecturer-position-at-the-university-of-strathclyde/2966 "2026-03-09T13:30:27Z")

</div>

The Mathematically Structured Programming research group at the University of Strathclyde is advertising a permanent position. We have several type theorists in the group (e.g. Conor McBride, Bob Atkey, Guillaume Alla…

---

## [Assistant professor position at Télécom Paris "Formal Methods at the crossroads of Hardware and Software"](https://discourse.rocq-prover.org/t/assistant-professor-position-at-telecom-paris-formal-methods-at-the-crossroads-of-hardware-and-software/2895)

<div class="topic-metadata">

**Author:** [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Replies:** 0\
**Last updated:** [January 9, 2026, 3:53pm UTC](https://discourse.rocq-prover.org/t/assistant-professor-position-at-telecom-paris-formal-methods-at-the-crossroads-of-hardware-and-software/2895 "2026-01-09T15:53:59Z")

</div>

A job vacancy under the title “Formal Methods at the crossroads of Hardware and Software” is open within the ACES (Autonomous, Critical, Embedded Systems) team of Télécom Paris. The position aims at strengthening the tea…

---

## [Several fully funded PhD and Postdoc positions in Quantum](https://discourse.rocq-prover.org/t/several-fully-funded-phd-and-postdoc-positions-in-quantum/2884)

<div class="topic-metadata">

**Author:** [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Replies:** 0\
**Last updated:** [December 17, 2025, 8:51pm UTC](https://discourse.rocq-prover.org/t/several-fully-funded-phd-and-postdoc-positions-in-quantum/2884 "2025-12-17T20:51:03Z")

</div>

We offer several fully funded PhD and Postdoc positions in Quantum Software (verification, compilation, optimization). Interested applicants with strong analytical skills and a desire to work on algorithmic and modeli…

---

## [UK home fees PhD position in Mathematically Structured Programming at Strathclyde](https://discourse.rocq-prover.org/t/uk-home-fees-phd-position-in-mathematically-structured-programming-at-strathclyde/2868)

<div class="topic-metadata">

**Author:** [@gallais](https://discourse.rocq-prover.org/u/gallais)\
**Replies:** 2\
**Last updated:** [December 7, 2025, 5:35pm UTC](https://discourse.rocq-prover.org/t/uk-home-fees-phd-position-in-mathematically-structured-programming-at-strathclyde/2868 "2025-12-07T17:35:25Z")

</div>

Hello Rocqers, I have pasted below the advertisement for UK home fees PhD positions in my team at Strathclyde (Glasgow, Scotland). Sorry about the tight turnaround time as the internal announcements were quite delayed…

---

## [PhD positions in Automated and Foundational Verification at ISTA](https://discourse.rocq-prover.org/t/phd-positions-in-automated-and-foundational-verification-at-ista/2863)

<div class="topic-metadata">

**Author:** [@MichaelSammler](https://discourse.rocq-prover.org/u/MichaelSammler)\
**Replies:** 0\
**Last updated:** [November 27, 2025, 9:50am UTC](https://discourse.rocq-prover.org/t/phd-positions-in-automated-and-foundational-verification-at-ista/2863 "2025-11-27T09:50:27Z")

</div>

I am excited to announce that I am recruiting PhD students to join my group at the Institute of Science and Technology Austria (ISTA), located on the outskirts of Vienna. I am looking for motivated and capable students w…

---

## [Full Professor position in Programming Languages at the University of Tartu](https://discourse.rocq-prover.org/t/full-professor-position-in-programming-languages-at-the-university-of-tartu/2847)

<div class="topic-metadata">

**Author:** [@danelahman](https://discourse.rocq-prover.org/u/danelahman)\
**Replies:** 0\
**Last updated:** [November 6, 2025, 9:12am UTC](https://discourse.rocq-prover.org/t/full-professor-position-in-programming-languages-at-the-university-of-tartu/2847 "2025-11-06T09:12:35Z")

</div>

The Institute of Computer Science at the University of Tartu in Estonia is currently advertising a Full Professor position in Programming Languages: https://ut.ee/en/job-offer/professor-programming-languages-0 Areas o…

---

## [AI for formal math researcher at Mistral AI](https://discourse.rocq-prover.org/t/ai-for-formal-math-researcher-at-mistral-ai/2831)

<div class="topic-metadata">

**Author:** [@jasonrute](https://discourse.rocq-prover.org/u/jasonrute)\
**Replies:** 0\
**Last updated:** [October 2, 2025, 4:14pm UTC](https://discourse.rocq-prover.org/t/ai-for-formal-math-researcher-at-mistral-ai/2831 "2025-10-02T16:14:33Z")

</div>

Thrilled to announce Mistral AI’s new formal math team following our $2B funding round. We’re looking for people at the crossroads of formal math (Lean, Rocq, etc…) and AI. We offer: Work on creating the state-of-the-…