Skip to content
Change the repository type filter

All

    Repositories list

    • Automatically extracts hidden invariants from plain English specifications and generates formal proofs using Lean 4. Connect your Jira, Confluence, or Google Do…
      Rust
      01026Updated Apr 15, 2026Apr 15, 2026
    • Cut vuln noise to near-zero by proving which CVEs are actually callable from your app’s entry points, using open CLIs, reproducible SBOMs, and CI-first workflow…
      Python
      Apache License 2.0
      0202Updated Apr 15, 2026Apr 15, 2026
    • Provable AI agents with behavioral guarantees enforced by formal verification, runtime security, and end-to-end audit trails.
      Rust
      Other
      210337Updated Apr 15, 2026Apr 15, 2026
    • A minimal, reusable CI template for running Lean 4 proofs on Morph Cloud's Infinibranch with intelligent caching and sharding.
      Python
      0100Updated Apr 15, 2026Apr 15, 2026
    • Continuous Integration system that automatically diagnoses, patches, and validates code issues using AI-powered analysis and formal verification.
      TypeScript
      MIT License
      0200Updated Apr 15, 2026Apr 15, 2026
    • Transforms raw runtime telemetry into machine-checked forensic evidence and proves that evidence can't be forged, lost, or silently falsified.
      Lean
      MIT License
      0205Updated Apr 15, 2026Apr 15, 2026
    • Runtime safety components for AI model inference with formal proofs, ultra-low latency, and guaranteed correctness.
      Lean
      MIT License
      0200Updated Apr 15, 2026Apr 15, 2026
    • Formal verification framework for dataset lineage, policy compliance, and training-time safety guarantees.
      Python
      MIT License
      0108Updated Apr 15, 2026Apr 15, 2026
    • Machine-checks every fixed model artefact—weights, vocab, quant tables, tokenizers.
      Python
      MIT License
      0102Updated Apr 15, 2026Apr 15, 2026
    • A testbed for validating and demonstrating Provability Fabric's capabilities with observability, safety case management, external agent integration, and automat…
      Python
      Apache License 2.0
      0200Updated Apr 15, 2026Apr 15, 2026
    • SpecCursor is a GitHub App that autonomously upgrades dependencies, patches regressions using AI, and proves invariants using Lean 4.20. It provides a complete …
      TypeScript
      MIT License
      0100Updated Apr 15, 2026Apr 15, 2026
    • morph-replay-runner is a command-line interface (CLI) tool designed to execute TRACE-REPLAY-KIT bundles with branch-N parallelism on Morph Cloud. This tool stre…
      Python
      0100Updated Apr 15, 2026Apr 15, 2026
    • Multiple SSE MCP servers behind a permissioning sidecar enforcing PERM-UNIFY-R1 (Call/Read/Write/Grant + epochs + IFC witnesses)
      Go
      MIT License
      0208Updated Apr 15, 2026Apr 15, 2026
    • Generate understanding, not just code. This toolkit helps teams reduce Time To Understanding (TTU) and Time To First Safe Change (TTFSC) with maps, traces, tour…
      HTML
      MIT License
      01012Updated Apr 15, 2026Apr 15, 2026
    • Lean Toolchain provides a collection of formally verified cryptographic algorithms, mathematical operations, and data parsing utilities. All implementations are…
      Lean
      MIT License
      0203Updated Apr 15, 2026Apr 15, 2026
    • Formally verified deployment-boundary guarantees: RBAC, tenant isolation, SGX/SEV attestation, and compliance artifact generation with machine-checked proofs.
      Rust
      MIT License
      01014Updated Apr 15, 2026Apr 15, 2026
    • SpecSync

      Public
      Formal specification system that automatically analyzes code changes and generates comprehensive formal specifications using advanced LLM techniques and Lean4 t…
      TypeScript
      MIT License
      0102Updated Apr 15, 2026Apr 15, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.