LemmaScript: verification toolchain for TypeScript

Cambridge, MA

Accelerating the development of LemmaScript through adoption, real-world use, and a training corpus that makes verification-first programming the default for future AI

Project Details

The proof-of-concept is strong and we are working toward a stable version (1.0). This project aims to tackle the adoption/development cycle. When we say “adoption,” we mean by both people and agents. To accelerate development of the toolchain and develop a robust ecosystem, we need human adoption and feedback. To make verification-first programming the default to agents, we need a large corpus of training materials for the next family of AI.

We can achieve both of these goals with similar activities:
1. Hold a hackathon
Output: 100s of new adopters + real-world projects built with LemmaScript

Run webinars and workshops focused on the concept of verification-first programming
Output: all materials made public, gather feedback, developer data + develop partnerships with larger organizations on similar tracks
Develop and distribute learning materials: documentation, tutorials, developer trainings, and community support to decrease the friction of getting started with the tooling and technology

Output: A full body of LemmaScript materials (case studies, docs, guides, examples, videos, etc).

In parallel to the previous 3 activities, continue to expand the LemmaScript ecosystem and its capabilities
Output: Release a stable version

Who’s involved:
Nada Amin: Drives the technical development of LemmaScript

Fernanda Graciolli: Informs toolchain design, and drives adoption and developer relations

Theory of Impact

In this case, the reduction in x-risk comes from the prevention of errors in critical code that could lead to catastrophic large-scale outcomes. Currently, much of AI-generated code is human-reviewed, but we are quickly moving toward a world where agents are the primary generators and reviewers of code, and as such, are given more and more autonomy to push production code that affects large groups of people. We already see a rising number of security breaches (e.g., CVEs) and buggy software (albeit lower-stakes) due to AI-generated code. In the near future, AI will inevitably be adopted in workflows that touch higher-stakes domains: critical infrastructure, authorization, financial systems, etc. In those domains, certain critical bugs mean catastrophic losses — in terms of how many are affected, in terms of the depth of the effect, or both. The development and adoption of formal external verifiers must begin long before AI is integrated into these critical paths, so that when they inevitably are integrated, we are equipped to prevent catastrophic mistakes altogether.

Furthermore, LemmaScript allows us to further explore agent safety by verifying the agents themselves: instead of relying on soft guardrails, LemmaScript allows us to embed hard contracts into agent actions that make it, not unlikely, but impossible that an agent will perform a forbidden action.

People

Fernanda Graciolli

Team Member

Nada Amin

Team Member

Grants Received– no grants recorded

Add grant

Funding Asks

grantmaking.ai Launch Round

Applied

Minimum

$32,000

Ideal

$63,000

What this ask is

This project is the first significant step toward a future where AI generated code is correct by default. We have developed LemmaScript, a verification toolchain for TypeScript that extends correctness from type-checking to behavioral contracts that can be formally verified. That means that, even before compiling the code, an entire class of bugs is eliminated by construction. We are building this toolchain for a future where agents write nearly 100% of implementation code. LemmaScript is a step toward a system that lives outside of AI judgment so that code generated and pushed by fully-autonomous agents carry guarantees of correctness established by an external verifier. In this case, the reduction in x-risk comes from the prevention of errors in critical code that could lead to catastrophic large-scale outcomes.

The proof-of-concept is strong and we are working toward a stable version (1.0). This project aims to tackle the adoption/development cycle. When we say “adoption,” we mean by both people and agents. To accelerate development of the toolchain and develop a robust ecosystem, we need human adoption and feedback. To make verification-first programming the default to agents, we need a large corpus of training materials for the next family of AI.

We can achieve both of these goals with similar activities:
1. Hold a hackathon
Output: 100s of new adopters + real-world projects built with LemmaScript

2. Run webinars and workshops focused on the concept of verification-first programming
Output: all materials made public, gather feedback, developer data + develop partnerships with larger organizations on similar tracks

3. Develop and distribute learning materials: documentation, tutorials, developer trainings, and community support to decrease the friction of getting started with the tooling and technology

Output: A full body of LemmaScript materials (case studies, docs, guides, examples, videos, etc).

4. In parallel to the previous 3 activities, continue to expand the LemmaScript ecosystem and its capabilities
Output: Release a stable version

Who’s involved:
Nada Amin (myself): I drive the technical development of LemmaScript

Fernanda Graciolli: Informs toolchain design, and drives adoption and developer relations

How the money will be spent

https://docs.google.com/spreadsheets/d/1YX7UVkfoczsCQ4OA5HcfsAz8ij77tto_JdnfJw6BiiE/edit?usp=sharing

Discussion

No comments yet. Be the first to share your thoughts.