diff --git a/extra/public/20240508-chapman.pdf b/extra/public/20240508-chapman.pdf
new file mode 100644
index 0000000..6f453af
Binary files /dev/null and b/extra/public/20240508-chapman.pdf differ
diff --git a/extra/public/20240522-far.pdf b/extra/public/20240522-far.pdf
new file mode 100644
index 0000000..51260cb
Binary files /dev/null and b/extra/public/20240522-far.pdf differ
diff --git a/extra/public/20240924-berkeley.pdf b/extra/public/20240924-berkeley.pdf
new file mode 100644
index 0000000..9bc9548
Binary files /dev/null and b/extra/public/20240924-berkeley.pdf differ
diff --git a/posts/2024-05-08-ai-assisted-coding-correct-by-construction-not-by-generation.md b/posts/2024-05-08-ai-assisted-coding-correct-by-construction-not-by-generation.md
new file mode 100644
index 0000000..1d4ae90
--- /dev/null
+++ b/posts/2024-05-08-ai-assisted-coding-correct-by-construction-not-by-generation.md
@@ -0,0 +1,17 @@
+---
+date: 2024-05-08
+excerpts: 2
+---
+
+# AI-assisted coding: correct by construction, not by generation
+
+## Abstract
+
+Atlas and Topos has been working on a roadmap for AI-assisted code specification and synthesis. The thesis is that formal verification (FV) is our best bet for protecting our sociotechnical systems, especially from human-led and/or AI-enabled attacks. Formal AI-assisted coding could make FV widespread and turn the tide in favor of defense. The roadmap describes concrete projects towards that goal. In this talk, I will discuss various components of the roadmap and show simple demos of what language models can do out of the box. I will also dive into correct-by-construction code synthesis, and how that it preferable to token-by-token code generation.
+
+## Details
+[Topos-Chapman Workshop](https://blogs.chapman.edu/scst/announcement/chapman-university-to-partner-with-topos-institute/)
+
+[Video](https://www.youtube.com/watch?v=rHY7nboIyBg)
+
+[Slides](https://w3id.org/people/shaoweilin/public/20240508-chapman.pdf)
diff --git a/posts/2024-05-22-formal-ai-assisted-code-specification-and-synthesis-concrete-steps-towards-safe-sociotechnical-systems.md b/posts/2024-05-22-formal-ai-assisted-code-specification-and-synthesis-concrete-steps-towards-safe-sociotechnical-systems.md
new file mode 100644
index 0000000..c0e1066
--- /dev/null
+++ b/posts/2024-05-22-formal-ai-assisted-code-specification-and-synthesis-concrete-steps-towards-safe-sociotechnical-systems.md
@@ -0,0 +1,17 @@
+---
+date: 2024-05-22
+excerpts: 2
+---
+
+# Formal AI-assisted code specification and synthesis: concrete steps towards safe sociotechnical systems
+
+## Abstract
+
+Atlas and Topos has been working on a roadmap for AI-assisted code specification and synthesis. The thesis is that formal verification (FV) is our best bet for protecting our sociotechnical systems, especially from human-led and/or AI-enabled attacks. Formal AI-assisted coding could make FV widespread and turn the tide in favor of defense. The roadmap describes concrete projects towards that goal. In this talk, I will discuss various components of the roadmap and show simple demos of what language models can do out of the box. I will also dive into correct-by-construction code synthesis, and how that it preferable to token-by-token code generation.
+
+## Details
+[FAR Seminar](https://far.ai/labs/#:~:text=FAR%20Seminar,Labs%20community.)
+
+[Video](https://www.youtube.com/watch?v=HDvN14dvy2g)
+
+[Slides](https://w3id.org/people/shaoweilin/public/20240522-far.pdf)
diff --git a/posts/2024-09-24-safety-by-shared-synthesis.md b/posts/2024-09-24-safety-by-shared-synthesis.md
new file mode 100644
index 0000000..af20954
--- /dev/null
+++ b/posts/2024-09-24-safety-by-shared-synthesis.md
@@ -0,0 +1,17 @@
+---
+date: 2024-09-24
+excerpts: 2
+---
+
+# Safety by shared synthesis
+
+## Abstract
+
+Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal verification (FV) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems. AI could allow widespread use of FV in years not decades, shifting cyber risks strongly in favor of defense. In this talk, I will outline our report with Atlas Computing on AI-enabled tools for scaling formal verification (https://atlascomputing.org/ai-assisted-fv-toolchain.pdf). I will also discuss some lessons that I learnt along the way, especially about shared synthesis - the collaborative construction of formal specifications, implementations and proofs.
+
+## Details
+[Topos Berkeley Semimar](https://topos.site/events/berkeley-seminar/index.html)
+
+[Video](https://youtu.be/N1qZhOU5OWo)
+
+[Slides](https://w3id.org/people/shaoweilin/public/20240924-berkeley.pdf)