Stars
Infinitely scalable research library storage & search for AI agents, backed by S3.
Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh
CLI that maps a spec to the code implementing it, and flags which links break when either side is edited
async language server protocol plugin for vim and neovim
Language Server Protocol (LSP) plugin for Vim9
A runnable verified-rewards loop: temporal-logic model checking as a reward oracle for LLM-generated code — verdicts, counterexample traces, reward construction
Qwen-AgentWorld: Language World Models for General Agents
Switchyard lets LLM applications route traffic across models and providers while preserving native OpenAI and Anthropic API compatibility - enabling flexible model selection, benchmarking, and cost…
Dafny verifies proofs; claimcheck confirms intent.
Requirements analysis and source intent alignment tool
A framework for scalable, distributed discovery systems.
A desktop reader for OpenSpec projects - browse changes, trace how requirements evolved, and comment on specs, all from local folders
The prover proves the present; the seal protects the past. An append-only freeze for verified contracts.
Make agents prove that their code is correct.
verification toolchain for TypeScript (Tech Preview)
⚡A CLI tool for code structural search, lint and rewriting. Written in Rust
Developer-friendly OSS embedded retrieval library for multimodal AI. Search More; Manage Less.
30 Agents Every AI Engineer Must Build, published by Packt
SysMD is a SysML v2/KerML tool with an intuitive, notebook-style interface that makes getting started easy. What truly sets SysMD apart is its integrated solver, enabling engineering calculations d…
This is the repo for a simple spec-driven workshop
Ralph loop + OpenSpec integration for Cursor, OpenCode and ClaudeCode heavy lifting.
OpenDST - Deterministic Simulation Testing for Java
The prototype tool of a JML generation technique (paper accepted in ICSE'25) for Java programs.
vACT: Verifiable specification synthesis with Spec-Harness feedback
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
A DuckDB Community Extension to enable Behavioral Analytics, inspired by ClickHouse.
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)