From d05c9066ee6c7833fbceee3ff76ab0ea02c0249a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 13 May 2024 11:49:05 +0200 Subject: [PATCH] feat: announce tutorial --- content/posts/announcement-tutorial.md | 44 ++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 content/posts/announcement-tutorial.md diff --git a/content/posts/announcement-tutorial.md b/content/posts/announcement-tutorial.md new file mode 100644 index 0000000..7e4f946 --- /dev/null +++ b/content/posts/announcement-tutorial.md @@ -0,0 +1,44 @@ +--- +author: "Lucas Franceschino" +title: "Announcing the hax tutorial" +date: "2024-05-13" +description: "We wrote a tutorial for hax!" +tags: ["tutorial", "announcement"] +ShowToc: false +ShowBreadCrumbs: false +--- + +We have been applying hax to verify several Rust pieces of software +recently. hax was used to verify [Libcrux's implementation of +ML-KEM](https://cryspen.com/post/ml-kem-verification/) with F*, but +also for [smart +contracts](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert) +verification with Coq, and even on +[protocols](https://github.com/cryspen/bertie) with F\* and our new +ProVerif backend. + +Meanwhile, we also presented hax at several conferences and +workshops. The need for more documentation and guidance was becoming +apparent: it was about time to have a tutorial! + +## New resources to learn more about hax + +The [hax book](https://hacspec.org/book/) has three new chapters: + - The [Quick start](https://hacspec.org/book/quick_start/intro.html) + chapter explains how to go from a simple Rust crate to an F* + extraction via hax, including how to install the tooling. + - The [Tutorial](https://hacspec.org/book/tutorial/index.html) + chapter goes more in-depth into using hax and F* together to prove + various properties of Rust code. + - The [FAQ](https://hacspec.org/book/faq/into.html) chapter is a work + in progress but is intended to answer pragmatically and with + examples to precise common issues or questions. Feel free to open + an issue on the [book + repository](https://github.com/hacspec/book/issues) if you feel like a topic should be addressed! + +We also added several examples of Rust verification via hax and F* in +the [example +directory](https://github.com/hacspec/hax/tree/main/examples) of hax, +please check them out! + +