Events and news relevant to the Laboratory for Foundations of Computer Science

[Paul Jackson <Paul.Jackson@ed.ac.uk>]

A reminder about Rod Chapman’s talk this Friday on "Formal is fast: verification and optimization of cryptographic code at AWS”.

From: aiai-members <aiai-members-bounces@inf.ed.ac.uk> on behalf of Informatics Institute News via aiai-members <aiai-members@inf.ed.ac.uk>
Date: Monday, 26 January 2026 at 09:32
To: inf-seminars@mlist.is.ed.ac.uk <inf-seminars@mlist.is.ed.ac.uk>, inf-aiai-seminars@mlist.is.ed.ac.uk <inf-aiai-seminars@mlist.is.ed.ac.uk>, AIAI Members <aiai-members@inf.ed.ac.uk>
Subject: [aiai-members] *REMINDER* AIAI Seminar: Friday 30th January 15:00, Room Bayes Theorem, Speaker Rod Chapman

 

Hello all,

 

There will be an AIAI Seminar on Friday 30th January in Bayes Theorem (G.03) by visiting speaker Rod Chapman.

 

Title: Formal is fast: verification and optimization of cryptographic code at AWS

 

Speaker: Dr Rod Chapman, Senior Principal Applied Scientist, AWS Cryptography

 

Abstract: This presentation will go over our approach to formal verification of cryptographic code at AWS, concentrating on our recent efforts with ML-KEM and ML-DSA. We'll cover our approach to assembly-language verification, and how we are verifying type-safety of C code within AWS-LC. Proof also enables "fearless optimization" of crypto code, where proofs of correctness and/or equivalence preserve functional behaviour while allowing and inspiring non-trivial performance improvements. We're also using automated super-optimization of assembly language for our Graviton processors to unlock performance gains on specific micro-architectures. These technical approaches will be illustrated by the mlkem-native library - an open-source implementation of the recently-standardized ML-KEM algorithm that combines formal verification with state-of-the-art performance on all major platforms.

 

Bio: Rod is a senior principal applied scientist within the Cryptography group of Amazon Web Services. He specializes in the design, development and verification of cryptographic software, and has particular experience with programming language design and automated reasoning technologies. He also coaches development teams and leadership in high-assurance software development disciplines, technologies,

and processes. He is a Fellow of the IET and an honorary visiting professor at the University of York.

 

Best wishes

Jodie

 

Jodie Cameron

Institute Administrator

Room 1.33

University of Edinburgh, Informatics Forum

10 Crichton St | Edinburgh | EH8 9AB

( Available on Microsoft Teams or email to arrange a phone call

Working hours: Mon, Tue, Wed, Thur, Fri – 09:00 – 17:00

 

 

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.


_______________________________________________
aiai-members mailing list
aiai-members@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/aiai-members