Public snapshots of "ACSL by Example"

Collection of resources for research concerning Machine Learning and Formal Methods.

Frama-C and WP tutorial

Overview of the Tree Borrows rules for detecting violations of the aliasing discipline in Rust

Slides and sources for talks on Tree Borrows

Examples for TLAPS (TLA+ Proof System)

Research and Development for Cybersecurity Engineering. Our mission is to develop a scientific theory of cybersecurity and a toolchain for the secure engineering of cyber-physical systems.

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

The CLEARSY Safety Platform Programming Handbook

My master thesis on information flow control on a minimal version of the RISC-V architecture with a model checker

Proving the correctness and performance of certain parallel algorithms

In this repository you can find all of my assignments for Formal Specification and Verification of Programs Course when I was in 1st semester of my master's at SUT.

MSc project on «Formal Verification of Rust with Stainless».

Homework project developed in the course FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (now FORMAL METHODS FOR SOFTWARE ENGINEERING) of Politecnico di Milano during the academic year 2024/2025. Mark: 30 cum laude

Formal specification for a UTxO wallet

Source code for the paper "Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions"

This project is developing a B specification of an Asteroids arcade game, using the B tools Atelier B & ProB

A modular, CI-verified formal manuscript that constructs a canonical trace-class operator whose spectral determinant encodes the completed Riemann zeta function—culminating in a spectral equivalence formulation of the Riemann Hypothesis. Includes DAG-audited proofs, Lean compatibility scaffolds, and agent-safe modular structure.

Android + Formal Methods