diff --git a/man.html b/man.html
index a30dc70..35fb66a 100644
--- a/man.html
+++ b/man.html
@@ -24,15 +24,15 @@
       <div class="section" id="name">
         <div class="section-title">Name</div>
         <div class="content">
-          Henri Saudubray - Computer science student
+          Henri Saudubray - PhD student
         </div>
       </div>
       <div class="section" id="synopsis">
         <div class="section-title">Synopsis</div>
         <div class="content">
-          I am a computer science student at Parisian Master of Research in
-          Computer Science (MPRI) at Universit&#xE9; Paris Saclay, focusing on
-          formal logic, proof assistants, and programming languages.
+          I am a PhD student at Laboratoire M&#xE9;thodes Formelles (LMF) at
+          Universit&#xE9; Paris Saclay, focusing on formal logic, proof
+          assistants, and programming languages.
         </div>
       </div>
       <div class="publications" id="publications">
@@ -60,6 +60,19 @@
       <div class="section" id="experience">
         <div class="section-title">Experience</div>
         <ul class="content">
+          <li>
+            <div class="title">
+              <a href="https://lmf.cnrs.fr">
+                Laboratoire M&#xE9;thodes Formelles,
+                Universit&#xE9; Paris Saclay</a>
+              - Since October 2025
+            </div>
+            <div class="description">
+              PhD. Working on the design and unification of programming,
+              specification and proof languages in the context of deductive
+              program verification, in the
+              <a href="https://www.why3.org">Why3</a> platform.
+          </li>
           <li>
             <div class="title">
               <a href="https://parkas.di.ens.fr">
@@ -67,11 +80,13 @@
               - March to August 2025
             </div>
             <div class="description">
-              M2 Internship. Working on reproducibility and transparency of
+              M2 Internship. Worked on reproducibility and transparency of
               assertions in the synchronous hybrid language
               <a href="https://zelus.di.ens.fr">Z&#xE9;lus</a>.
-              Definition of a formal semantics for a multi-solver language
-              back-end.
+              Designed and implemented a
+              <a href="https://codeberg.org/17maiga/hsim">
+                formal executable semantics
+              </a> for a multi-solver language runtime.
             </div>
           </li>
           <li>
@@ -83,7 +98,7 @@
             <div class="description">
               M1 Internship. Added support for case analysis and proofs by
               induction on inductive predicates in the
-              <a href="https://www.why3.org">Why3</a> framework.
+              <a href="https://www.why3.org">Why3</a> platform.
               Translated a Coq proof to Why3 as a test.
             </div>
           </li>
@@ -176,6 +191,12 @@
             </div>
             <div class="description">Report for M1 Internship.</div>
           </li>
+          <li>
+            <div class="title">
+              <a href="./pdf/m2_report.pdf">/pdf/m2_report.pdf</a>
+            </div>
+            <div class="description">Report for M2 Internship.</div>
+          </li>
         </ul>
       </div>
       <div class="section" id="see_also">
@@ -183,8 +204,8 @@
         <ul class="content">
           <li>
             <div class="title">
-              <a href="mailto:henri.saudubray@proton.me"
-                 >henri.saudubray[at]proton[dot]me</a>
+              <a href="mailto:hms@lmf.cnrs.fr"
+                 >hms[at]lmf[dot]cnrs[dot]fr</a>
             </div>
             <div class="description">Email address.</div>
           </li>
@@ -205,8 +226,8 @@
       </div>
     </main>
     <footer>
-      <span>1.3.0</span>
-      <span>2025-03-24&nbsp;</span>
+      <span>1.4.0</span>
+      <span>2025-10-03&nbsp;</span>
       <span>HENRI(1)</span>
     </footer>
   </body>
diff --git a/pdf/m2_report.pdf b/pdf/m2_report.pdf
new file mode 100644
index 0000000..7e05ada
Binary files /dev/null and b/pdf/m2_report.pdf differ