Projects

Community Building

We're advancing a new AI architecture that provides provable safety properties by constraining AI outputs with specifications. Advancing a new architecture requires increasing the number of people aware of and working on this architecture until it's a ubiquitous mechanism for assuring safety.

Spreadsheet

Neglected catastrophic risks from AI

We've started a list of potential risks that would noticably and negatively affect most humans if they came to pass.

We consider a problem neglected if there isn't someone full-time focused solving it.

We'll announce the launch on our blog

Mailing List

Community mailing list on Guaranteed Safe AI

We started a public google group mailing list dedicated to discussing AI architectures designed to have provable safety properties.

You can see past conversations or join directly

Join the conversation

Events

Current and past events

See the events that we have and are looking forward to organizing or co-organizing!

If you'd like to organize something with us, please email us at [email protected]

See our events page

Cyber

We think AI shouldn't be a black box to users, but instead should output a formal specification of solution properties as a reviewable intermediary result. The first step is building tools that (1) help users generate specifications for software, (2) generate programs from those specifications, and (3) generate proofs that the programs satisfy the specifications. Our early experiments are focused on understanding and describing the state-of-the-art research on the intersection of AI and formal methods, laying the foundations to build these tools.

Project

Specification IDE

We're prototyping a tool to show users with no formal methods experience could understand a formal specification; the tool maps subsections of that spec to natural language description and annotates the comparison

See the code here

Whitepaper (2-pager)

The Opportunity for AI and FV

A nontechnical explanation of (1) why AI poses a cybersecurity risk, (2) the value and difficulties in deploying formal verification (FV), (3) how advances in language models could overcome these limits, and (4) next steps to advance the usage of formal verification.

Read the 2-pager

Experiment

Porting Libraries Between Coq and Lean with ChatGPT

At Atlas, Jason Gross developed a testbed to demonstrate that language models are sufficiently capable to convert from Coq proofs to Lean proofs by developing an verification tool to show that compiled Coq proofs and transpiled Lean proofs were equivalent to isomorphism.

Read more

Report

AI Assisted FV Toolchain

Formally verifying software involves generating (a) the software itself, (b) a specification of how the software should behave, and (c) a mathematical proof that the software satisfies the specification.

View report

Want to get involved?

Interested in quarterly updates?
Get email updates
Want more frequent updates?
Follow our blog