Skip to content

@AU-COBRA Concordium Blockchain Research Center Aarhus

Change the repository type filter

All

    Repositories list

    11 repositories

    • lambda-box-extraction

      Public
      Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml
      coqextraction
      Rocq Prover
      •
      MIT License
      •2•8•0•1•Updated Nov 5, 2025Nov 5, 2025

    • coq-rust-extraction

      Public
      Coq plugin for extracting Rust code
      rustcoqextraction
      Rocq Prover
      •
      MIT License
      •4•13•9•0•Updated Oct 27, 2025Oct 27, 2025

    • extraction-results

      Public
      A repository containing code extracted using ConCert
      rustsmart-contractsligoconcordium
      Rust
      •
      MIT License
      •0•1•0•0•Updated Oct 27, 2025Oct 27, 2025

    • coq-elm-extraction

      Public
      Coq plugin for extracting Elm code
      elmcoqextraction
      Rocq Prover
      •
      MIT License
      •1•2•0•0•Updated Oct 27, 2025Oct 27, 2025

    • ConCert

      Public
      A framework for smart contract verification in Coq
      smart-contractsblockchaincoqverification
      Rocq Prover
      •
      MIT License
      •22•124•5•1•Updated Oct 27, 2025Oct 27, 2025

    • OVN

      Public
      Verified implementation of the Open Vote Network protocol
      Rocq Prover
      •
      MIT License
      •2•1•0•0•Updated Aug 26, 2025Aug 26, 2025

    • AUCurves

      Public
      Synthesis of Formally Verified Cryptographic Primitives
      Coq
      •
      MIT License
      •1•10•0•0•Updated Jul 26, 2023Jul 26, 2023

    • typed-extraction

      Public archive
      Verified coq extraction
      coqverification
      Coq
      •
      MIT License
      •2•3•0•0•Updated Mar 26, 2023Mar 26, 2023

    • fiat-crypto

      Public
      Cryptographic Primitive Code Generation by Fiat
      Coq
      •
      Other
      •157•0•0•0•Updated Apr 24, 2022Apr 24, 2022

    • concordium-extracted-contracts

      Public archive
      Rust contracts for the Concordium blockchain extracted from the Coq development in ConCert
      Rust
      •0•2•0•0•Updated Jun 30, 2021Jun 30, 2021

    • PoS-NSB

      Public
      A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq
      Coq
      •
      MIT License
      •2•25•0•0•Updated Jan 21, 2021Jan 21, 2021