23Program Verification

43 entries

Std.Do / mvcgenBuilt-in monadic program logic and verification condition generator for do code.
LoomFramework for building multi-modal verifiers of effectful programs.verse-lab/loom
VelvetAuto-active program verifier.verse-lab/velvet
VeilAutomated and interactive verification of distributed protocols and transition systems.verse-lab/veil
Iris-LeanPort of the Iris higher-order concurrent separation logic framework.leanprover-community/iris-lean
LentilLTL reasoning infrastructure.verse-lab/Lentil
LeanSSRSSReflect-style tactic language.verse-lab/lean-ssr
lean-machinesModelling and refinement of stateful systems.lean-machines-central/lean-machines
leanSpecProgram specification in Lean 4.paulch42/lean-spec
WybeCoderAgentic verified imperative code generation on Loom/Velvet.facebookresearch/wybecoder

AeneasTranslates safe Rust to Lean for verification.AeneasVerif/aeneas
haxExtracts Rust code to Lean (and other backends).cryspen/hax
StrataPlatform for formalizing language syntax and semantics through extensible dialects and building automated reasoning tools on them.strata-org/Strata
LemmaScriptVerification toolchain for TypeScript (tech preview).midspiral/LemmaScript
rust-lean-modelsLean models of Rust standard library functions.model-checking/rust-lean-models
ACL2LeanReplay ACL2 proofs as kernel-checked Lean theorems.OathTech/ACL2Lean
TalosWebAssembly interpreter and weakest-precondition calculus for verifying WebAssembly modules.cajal-technologies/talos
lean-mlirMLIR semantics and verified peephole rewrites.opencompl/lean-mlir

Wasm.leanWebAssembly implementation.argumentcomputer/Wasm.lean
lean-wasmFormalization of the WebAssembly spec.T-Brick/lean-wasm
haskell-specFormal specification of the Haskell Language Report.haskell-spec/haskell-spec
graphql-leanFormalization of the GraphQL specification.duckki/graphql-lean
ELFSageELF parser and validator.draperlaboratory/ELFSage
SHerLOCStableHLO analyzer.leanprover/SHerLOC
TenCertVerified tensor compilation.leanprover/TenCert
graphitiVerified graph rewriting for dataflow circuits.VCA-EPFL/graphiti
lean-yjsVerification of the Yjs CRDT integration algorithm.iasakura/lean-yjs
langlibEsoteric programming languages, formally.ilyasergey/langlib

cedar-specLean specification and verification of AWS's Cedar authorization language, used for differential testing of the production implementation.cedar-policy/cedar-spec
SampCertVerified differential privacy, used in production by AWS Clean Rooms.leanprover/SampCert
VCVioMachine-checked cryptographic proofs with oracle computations.Verified-zkEVM/VCVio
DyLeanSymbolic analysis of cryptographic protocols.BobDyLean/dylean
verified-3d-mesh-intersectionVerified 3D constructive solid geometry.schildep/verified-3d-mesh-intersection
bitrepRust crate for bit-identical float reductions, with the merge algebra proved in Lean.KyleClouthier/bitrep

EVMYulLeanExecutable formal model of the EVM and Yul.NethermindEth/EVMYulLean
evm-smithFramework for AI systems to write EVM bytecode and prove it safe.leonardoalt/evm-smith
BlancMinimal EVM contract language, with proofs about the deployed bytecode.skbaek/blanc
CleanDSL for ZK circuits with soundness and completeness proofs (zk.golf).Verified-zkEVM/clean
ArkLibFormally verified arguments of knowledge.Verified-zkEVM/ArkLib
zkLeanDSL for specifying zero-knowledge statements.GaloisInc/zkLean
risc0-lean4Model of the RISC Zero zkVM.risc0/risc0-lean4
aegisVerify Cairo contracts.lindy-labs/aegis
btc-verifiedVerified Bitcoin serialization, txids and Merkle commitments.ProofOfKeags/btc-verified