-
Jet Propulsion Laboratory
- Pasadena, Califormia
Stars
Example specifications for the Lean Machines modelling framework
a Lean4 framework for the modeling and refinement of stateful systems
Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
A C++ babeltrace2 plugin which replaces ROS 2 Tracing
Kontroll demonstates how to control the Keymapp API, making it easy to control your ZSA keyboard from the command line and scripts.
LLMs as Copilots for Theorem Proving in Lean
NASA Open Source ION Software implementation of Delay Tolerant Networking. ION development is managed by the Jet Propulsion Lab; regression testing and code management are provided by Ohio University.
VS Code extension that allows you to record and play back guided tours of codebases, directly within the editor.
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Proving leftpad correct two-dozen different ways
🖥 Securely transfer and send anything between computers with TUI.
`@ifdef` is an annotation that implements conditional compilation in Scala
Qualitative Reasoning: Spatio-Temporal Reasoning using Relation Algebras and Constraint Networks. Documentation is under construction at ReadTheDocs. See link below.
Lean 4 programming language and theorem prover
A package for compositional system analysis and design
A zero-knowledge Lean4 compiler and kernel
Highly extensible platform for developers to better understand the complexity of Kubernetes clusters.
A gradle plugin that lets you define Exec and JavaExec tasks that run in the background
CLI and library for diff, patch, and ETL operations on CUE, JSON, and Yaml