Meta tags:
author=The Formosa team;
description=The Formosa project federates multiple tools and projects in machine-checked cryptography and high-assurance cryptographic engineering under a single banner, to better support developers and users.;

Headings (most frequently used words):

formosa, news, tools, projects, people, affiliations, and, supporters,

Text of the page (most frequently used words):
and (31), #formosa (25), the (20), for (13), institute (12), jasmin (12), security (11), max (10), planck (10), privacy (10), projects (9), 2026 (9), project (8), repository (8), university (7), universidade (7), tool (7), high (6), inesc (6), tec (6), verified (6), available (6), assurance (5), cryptographic (5), support (5), porto (5), formally (5), implementation (5), new (5), read (5), tools (4), cryptography (4), crypto (4), inria (4), centre (4), kem (4), version (4), announcement (4), release (4), compiler (4), federates (3), multiple (3), machine (3), checked (3), engineering (3), under (3), single (3), banner (3), better (3), developers (3), users (3), institutions (3), its (3), université (3), wing (3), dsa (3), keccak (3), libjade (3), easycrypt (3), implementations (3), website (3), news (3), team (2), supported (2), are (2), supporters (2), vincent (2), sandboxaq (2), virginia (2), tech (2), eindhoven (2), technology (2), haslab (2), minho (2), côte (2), azur (2), software (2), people (2), more (2), 25519 (2), with (2), major (2), minor (2), public (2), key (2), september (2), org, addition, other, have, constituent, financially, gratefully, acknowledge, their, component, variety, funders, our, active, members, work, following, affiliations, ruhr, bochum, yuval, yarom, xingyu, xie, lorraine, laporte, hwang, tiago, oliveira, swarn, priya, santiago, arranz, olmos, rui, fernandes, pqshield, pierre, yves, strub, radboud, peter, schwabe, miguel, quaresma, matthias, meijers, manuel, barbosa, luís, esquível, lionel, blatter, rosenpass, karolin, varner, joão, diogo, duarte, josé, bacelar, almeida, jean, christophe, léchenet, hugo, pacheco, henrique, faria, gustavo, delerue, imdea, gilles, barthe, cryptoexperts, uclouvain, gaëtan, cassiers, bristol, françois, dupressoir, hochschule, darmstadt, fabio, campos, input, output, taltech, denis, firsov, deirdre, connolly, hasso, plattner, potsdam, germany, chitchanok, chuengsatiansup, benjamin, grégoire, basavesh, ammanaghatta, shivakumar, cloudflare, bas, westerbaan, andreas, hülsing, boston, alley, stoughton, paris, adrien, koutsos, aaron, kaiser, hybrid, related, functions, sha3, shake, etc, x25519, library, written, computer, proof, correctness, primary, focus, offer, post, quantum, primitives, this, listed, detailed, page, workbench, speed, aim, being, efficient, safe, correct, secure, toolset, reasoning, about, relational, properties, probabilistic, computations, adversarial, code, main, application, construction, verification, game, based, proofs, march, april, july, had, expired, valid, one, annoncement, update, pgp, debian, packages, join, zulip, publications,

Text of the page (random words):
formosa crypto the formosa project federates multiple tools and projects in machine checked cryptography and high assurance cryptographic engineering under a single banner to better support developers and users news people tools projects publications formosa supporters the formosa crypto project federates multiple projects in machine checked cryptography and high assurance cryptographic engineering under a single banner to better support developers and users join us on zulip formosa news release 2026 09 0 of the jasmin compiler september 30 2026 a new major version of jasmin is available read the announcement update of the pgp public key of debian packages september 4 2026 the public key had expired and a new valid one is available read the annoncement release 2026 03 2 of the jasmin compiler july 16 2026 a new minor version of jasmin is available read the announcement release 2026 03 1 of the jasmin compiler april 14 2026 a new minor version of jasmin is available read the announcement release 2026 03 0 of the jasmin compiler march 9 2026 a new major version of jasmin is available read the announcement more news formosa tools easycrypt tool website tool repository easycrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code its main application is the construction and verification of game based cryptographic proofs jasmin tool website tool repository jasmin is a workbench for high assurance and high speed cryptography jasmin implementations aim at being efficient safe correct and secure libjade tool website tool repository libjade is a cryptographic library written in jasmin with computer verified proof of correctness and security in easycrypt the primary focus of libjade is to offer high assurance software implementations of post quantum crypto primitives the implementations available in this tool are listed and detailed in the formosa projects page formosa projects formosa 25519 project repository formosa 25519 is a formally verified implementation of x25519 formosa keccak project repository formosa keccak is a formally verified implementation of keccak and related functions sha3 shake etc formosa ml dsa project repository formosa ml dsa is a formally verified implementation of ml dsa formosa ml kem project repository formosa ml kem is a formally verified implementation of ml kem formosa x wing project repository formosa x wing is a formally verified implementation of x wing hybrid kem more projects formosa people aaron kaiser max planck institute for security and privacy adrien koutsos inria centre de paris alley stoughton boston university andreas hülsing eindhoven university of technology bas westerbaan cloudflare basavesh ammanaghatta shivakumar virginia tech benjamin grégoire inria centre d université côte d azur chitchanok chuengsatiansup hasso plattner institute and university of potsdam germany deirdre connolly sandboxaq denis firsov input output taltech fabio campos hochschule darmstadt françois dupressoir university of bristol gaëtan cassiers cryptoexperts and uclouvain gilles barthe max planck institute for security and privacy imdea software institute gustavo delerue universidade do porto henrique faria universidade do minho inesc tec hugo pacheco universidade do porto inesc tec jean christophe léchenet inria centre d université côte d azur josé bacelar almeida universidade do minho haslab inesc tec joão diogo duarte universidade do porto inesc tec karolin varner max planck institute for security and privacy rosenpass e v lionel blatter max planck institute for security and privacy luís esquível universidade of porto inesc tec manuel barbosa universidade do porto haslab inesc tec matthias meijers eindhoven university of technology tu e miguel quaresma max planck institute for security and privacy peter schwabe max planck institute for security and privacy radboud university pierre yves strub pqshield rui fernandes max planck institute for security and privacy santiago arranz olmos max planck institute for security and privacy swarn priya virginia tech tiago oliveira sandboxaq vincent hwang max planck institute for security and privacy vincent laporte inria centre de l université de lorraine xingyu xie max planck institute for security and privacy yuval yarom ruhr university bochum formosa affiliations and supporters formosa and its component projects are supported by a variety of funders and institutions our active members work for the following institutions in addition other institutions support and have supported formosa or its constituent projects financially we gratefully acknowledge their support the formosa team team formosa crypto org the formosa project federates multiple tools and projects in machine checked cryptography and high assurance cryptographic engineering under a single banner to better support developers and users