cedar-policy / cedar-specLinks
Definitional implementation of Cedar language and utilities for DRT
☆138Updated this week
Alternatives and similar repositories for cedar-spec
Users that are interested in cedar-spec are comparing it to the libraries listed below
Sorting:
- A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development sna…☆148Updated last week
- SampCert : Verified Differential Privacy☆82Updated 6 months ago
- Lean 4 port of Iris, a higher-order concurrent separation logic framework☆128Updated this week
- AWS Encryption SDK☆53Updated this week
- A mechanisation of Wasm in Coq(Rocq)☆110Updated 2 months ago
- Forge: A Tool and Language for Teaching Formal Methods☆91Updated this week
- Visual Studio Code Extension and Language Server Protocol for Rocq / Coq☆191Updated this week
- Lean 4 kernel / 'external checker' written in Lean 4☆127Updated 3 weeks ago
- A Lean library for Computer Science☆149Updated this week
- Tactics for discharging Lean goals into SMT solvers.☆236Updated this week
- RFCs for Cedar☆18Updated this week
- An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.☆150Updated last month
- Wasm SpecTec specification tools☆76Updated 2 weeks ago
- Separation Logic Proofs in Lean☆45Updated 7 months ago
- This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal…☆60Updated 2 weeks ago
- Companion files for Logical Verification 2020–2021 at VU Amsterdam☆96Updated 4 years ago
- Coq plugin embedding elpi☆177Updated this week
- ☆186Updated this week
- 🦖 Implementations of various type inference algorithms. The new project is now at https://github.com/cu1ch3n/type-inference-zoo-frontend…☆150Updated 4 months ago
- A formal consistency proof of Quine's set theory New Foundations☆73Updated 4 months ago
- The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)☆70Updated last year
- A foundational framework for modular cryptographic proofs in Coq☆69Updated 3 weeks ago
- A verification toolchain for Rust programs☆421Updated last week
- Verifying concurrent storage and distributed systems☆206Updated this week
- Rewrites TLA⁺ specs to use Unicode symbols instead of ASCII, and vice-versa☆40Updated 3 months ago
- The Steel separation logic library for F*☆36Updated 3 weeks ago
- Canonical is a performant sound and complete type inhabitation solver for dependent type theory.☆75Updated last week
- ☆58Updated last month
- Logic and Mechanized Reasoning☆107Updated last week
- Coq Protocol Playground with Se(xp)rialization of Internal Structures.☆133Updated last month