Skip to content

@secure-foundations Secure Foundations Lab

Change the repository type filter

All

    Repositories list

    42 repositories

    • owl

      Public
      Compositional Verification of Security Protocols
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •2•30•4•3•Updated Feb 19, 2026Feb 19, 2026

    • vest

      Public
      High-assurance and performant Rust-based parsing and serialization of binary data formats verified in Verus
      Rust
      •
      MIT License
      •9•46•5•1•Updated Feb 12, 2026Feb 12, 2026

    • trex-usenix25

      Public
      Top-level companion software artifact for the paper "TRex: Practical Type Reconstruction for Binary Code"
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •1•5•0•0•Updated Jan 31, 2026Jan 31, 2026

    • mariposa

      Public
      SMT
      •
      MIT License
      •8•16•6•1•Updated Jan 31, 2026Jan 31, 2026

    • tree-sitter-verus

      Public
      JavaScript
      •
      MIT License
      •1•6•1•2•Updated Nov 24, 2025Nov 24, 2025

    • trex

      Public
      🦖 Reconstruct Types from Binary Code
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •3•45•0•0•Updated Nov 21, 2025Nov 21, 2025

    • verdict

      Public
      Formally Verified X.509 Certificate Validation
      Rust
      •
      Apache License 2.0
      •0•11•0•0•Updated Nov 19, 2025Nov 19, 2025

    • riptide-verification

      Public
      Python
      •0•6•0•0•Updated Nov 11, 2025Nov 11, 2025

    • human-eval-verus

      Public
      Rust
      •
      MIT License
      •13•23•0•1•Updated Oct 1, 2025Oct 1, 2025

    • verdict-bench

      Public
      Benchmarking tools for various X.509 implementations against Verdict
      Python
      •0•1•0•0•Updated May 9, 2025May 9, 2025

    • axiom-profiler-2

      Public
      The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
      Rust
      •
      Apache License 2.0
      •5•1•0•0•Updated May 1, 2025May 1, 2025

    • leaf

      Public
      Leaf library for Iris Concurrent Separation Logic
      Coq
      •
      Other
      •0•9•0•0•Updated Apr 30, 2025Apr 30, 2025

    • mariposa-D_VBKV

      Public
      Dafny
      •2•0•0•0•Updated Feb 2, 2025Feb 2, 2025

    • trie-hard

      Public
      Novel implementation of a Trie data structure optimized for small, sparse maps
      Rust
      •
      Apache License 2.0
      •16•1•0•0•Updated Jan 27, 2025Jan 27, 2025

    • ironsync-osdi2023

      Public
      IronSync paper artifact for OSDI 2023
      Dafny
      •
      Other
      •0•2•0•0•Updated Sep 8, 2024Sep 8, 2024

    • veri-datalog

      Public
      Verified Datalog
      Dafny
      •2•5•0•0•Updated Aug 2, 2024Aug 2, 2024

    • mariposa-data

      Public
      SMT
      •1•0•0•0•Updated Mar 21, 2024Mar 21, 2024

    • wabt-732

      Public
      The WebAssembly Binary Toolkit
      C++
      •
      Apache License 2.0
      •796•0•0•0•Updated Mar 20, 2024Mar 20, 2024

    • Mariposa-Ironclad

      Public
      The MSR Ironclad project builds provably secure and reliable systems.
      Dafny
      •
      Other
      •59•0•0•0•Updated Jan 23, 2024Jan 23, 2024

    • burrow

      Public
      Burrow coq formalization
      Coq
      •
      Other
      •0•1•0•0•Updated Jan 17, 2024Jan 17, 2024

    • rWasm

      Public
      A cross-platform high-performance provably-safe sandboxing Wasm-to-native compiler
      Rust
      •8•42•1•3•Updated Jan 14, 2024Jan 14, 2024

    • veri-titan

      Public
      Verifying OpenTitan
      Dafny
      •
      MIT License
      •4•28•1•0•Updated Aug 20, 2023Aug 20, 2023

    • dafny

      Public
      Dafny is a verification-aware programming language
      C#
      •
      Other
      •300•4•13•2•Updated Jul 6, 2023Jul 6, 2023

    • dafny-exercise

      Public
      Dafny
      •
      Other
      •0•0•0•0•Updated Mar 23, 2023Mar 23, 2023

    • SWISS

      Public
      Automatically synthesizing invariants of distributed systems
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •2•9•0•0•Updated Dec 1, 2022Dec 1, 2022

    • verifiable-computation

      Public
      Code for the Pinocchio and Geppetto Verifiable Computation systems
      F#
      •
      Other
      •0•6•0•0•Updated Oct 31, 2022Oct 31, 2022

    • iron-sync

      Public
      Iron Sync concurrent verification framework
      Dafny
      •
      Other
      •0•0•0•0•Updated Oct 25, 2022Oct 25, 2022

    • provably-safe-sandboxing-wasm-usenix22

      Public
      Top-level companion software artifact for the paper "Provably-Safe Multilingual Software Sandboxing using WebAssembly"
      WebAssembly
      •
      BSD 3-Clause "New" or "Revised" License
      •1•38•0•0•Updated Aug 30, 2022Aug 30, 2022

    • wasm-semantics-fuzzer

      Public
      An aid for developing correct WebAssembly implementations through generative fuzzing
      Rust
      •
      BSD 3-Clause "New" or "Revised" License
      •2•15•0•0•Updated Aug 30, 2022Aug 30, 2022

    • vWasm

      Public
      A formally-verified provably-safe sandboxing Wasm-to-native compiler
      OCaml
      •
      BSD 3-Clause "New" or "Revised" License
      •1•28•0•0•Updated Aug 30, 2022Aug 30, 2022