A Tool-Chain for High-Assurance Cryptographic Software. - José Bacelar Almeida; Manuel Barbosa; Hugo Pacheco 001; Vitor Pereira 002 (ERCIM News, 2016)

A Fast and Verified Software Stack for Secure Function Evaluation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2017)

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (IACR Cryptol. ePrint Arch., 2018)

A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation. - Karim Eldefrawy; Vitor Pereira 002 (CCS, 2019)

A Machine-Checked Proof of Security for AWS Key Management Service. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Matthew Campagna; Ernie Cohen; Benjamin Grégoire; Vitor Pereira 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (IACR Cryptol. ePrint Arch., 2019)

A High-Assurance, Automatically-Synthesized, Evaluator for Machine-Checked (Proactively) Secure Multi-Party Computation. - Karim Eldefrawy; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2019)

Integrated Verification of Cryptographic Security Proofs and Implementations - Vitor Pereira 002 (2020)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Carlos Bacelar Almeida; Manuel Barbosa; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (CoRR, 2021)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Bacelar Almeida; Manuel Barbosa; Manuel L. Correia; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2021)

A formal treatment of the role of verified compilers in secure computation. - José Carlos Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (J. Log. Algebraic Methods Program., 2022)

Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. - Samuel Dittmer; Karim Eldefrawy; Stéphane Graham-Lengrand; Steve Lu 001; Rafail Ostrovsky; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2023)