Pinned Repositories
cemetery
A (toy-ish) DSL for Cryptography.
hacl-star
HACL*, a formally verified cryptographic library written in F*
lcc.cls
Clase de LaTeX para documentos de la LCC (prácticas, exámenes, etc)
ray-tracer
A pretty standard constructive solid geometry ray tracer
snake86
x86 Bootable Snake game
verificacion-con-fstar-2024
Repositorio de la optativa para la FCEIA
mtzguido's Repositories
mtzguido/verificacion-con-fstar-2024
Repositorio de la optativa para la FCEIA
mtzguido/hacl-star
HACL*, a formally verified cryptographic library written in F*
mtzguido/batteries-included
Batteries Included project
mtzguido/dotfiles_cs
temp
mtzguido/everest
mtzguido/everparse
Automated generation of provably secure, zero-copy parsers from format specifications
mtzguido/everquic-crypto
Security model and verified implementation of QUIC packet encryption in Low*, built over EverCrypt and EverParse.
mtzguido/FStar
A Proof-oriented Programming Language
mtzguido/fstar-mode.el
Emacs support for F*
mtzguido/fstar-project-template
A template for an F* project with Makefile and devcontainer
mtzguido/gci-download
mtzguido/gci-upload
mtzguido/git
Git Source Code Mirror - This is a publish-only repository but pull requests can be turned into patches to the mailing list via GitGitGadget (https://gitgitgadget.github.io/). Please follow Documentation/SubmittingPatches procedure for any of your improvements.
mtzguido/jobserver-sharing
mtzguido/karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code
mtzguido/ld_preload
LD_PRELOAD example
mtzguido/merkle-tree
A verified Merkle Tree, built as a standalone project on top of EverCrypt
mtzguido/mitls-fstar
Verified implementation of TLS 1.3 in F*
mtzguido/mtzguido.github.io
mtzguido/pulse
The Pulse separation logic DSL for F*
mtzguido/pulse-project
Base Pulse project (TODO: coallesce with FStarLang/pulse-sandbox)
mtzguido/ramon
Resource measurement tool
mtzguido/runlim
mtzguido/set-opam-env
mtzguido/steel
The Steel separation logic library for F*
mtzguido/VimFStar
A Vim mode for FStar
mtzguido/z3
The Z3 Theorem Prover
mtzguido/z3-fstar-testing
mtzguido/z3-ramon-results
mtzguido/z3-solver-comparison