Guardrails: Atomic

Homepage
Specification Generation Page
Verification Page
Generated Verified Code
Examples of Specifications

Inspiration

Traditional software testing - however elaborate - operates by sampling the space of possible behaviors. Tests are written for scenarios that we the developers think may happen, but our minds have limits. This limit is especially prevalent with respect to complex, real-life use of distributed systems. Consider a money transfer between 3 accounts, with 2 concurrent operations, under real-life constraints where network may not be reliable and the system may crash for various reasons at any time; the number of possible execution interleavings grows at rates beyond the rate of growth a test suite can afford to be.

Formal verification, on the other hand, does not depend on samples; rather, it leans on mathematical proofs to ensure that the behavior of the program is verified correct for the entire set of possible inputs! Companies ranging from AWS to Galois use formally verified software for their critical components.

But, if they're that great, why aren't they everywhere already? That is because programming with formal verification in mind is difficult - which leaves companies in a paradox: either to leverage the productivity afforded by AI, or to build software that is verified.

What if we want the best of both worlds?

What it does

Given a prompt, a YAML-formatted specification is generated. This specification can then be transformed into a Z3 Theorem Prover, a formal specification language. Because it is formally specified, it can be proven either false (with a counterexample), or pass, at which point the code is considered formally verified.

How we built it

We extensively leveraged Claude AI to deliver this large-scale project within the constraints of the hackathon time limit. The project is built in TypeScript, with pnpm. LLM AI is sourced via OpenRouter, so that we can choose the LLM best for each task.

Challenges we ran into

An issue we encountered was with MongoDB, where the data isn't sent to the database. This is due to our User IDs being stored as null, instead of an actual value, resulting in the database function not being called. We fixed the issue by associating the User ID with all calls.

Another challenge we had is our decision-making process between different formal verification langauges. We initially chose TLA+ because of its wide usage, and because one of our teammates had experience using TLA+. However, it emerged that TLA+ has syntactic intricacies that make AI-based generation from specification difficult to get correct, and that its counterexample checking requires the use of TLC, which is Java-based, hence requiring Docker, resulting in additional complexity. A decision was made to move to Z3 Theorem Prover towards the second half of the hackathon, and we were able to successfully complete the migration despite limited time, achieving better functionality based on our tests.

Accomplishments that we're proud of

We got the code to work! Given how tight the timeframe is, we are genuinely proud of our ability to collaborate efficiently on such a short timeframe. We are especially proud of the well-engineered and well-thought architecture: by planning out the workflow early on the hackathon, we are able to move fast throughout the hackathon, effectively dividing up tasks and progressing on multiple fronts simultaneously.

What we learned

In the technical sphere, we learned about the power of modular LLM providers and unified development frameworks. In my experience, hackathon projects would often get stuck over bugs that emerge halfway through a functionality's implementation, stalling progress for hours on end because of compatibility issues. By leveraging the NextJS unified architecture, we were mostly exempt from such blockers, as it natively handles the systems and use cases we envisioned. The modular LLM (openrouter) provides us with the flexibility to experiment with and leverage different LLM models across providers with ease, empowering us to optimize our project's performance.

We also learned that formal verification remains to be a challenging space. Seeing the generated Z3 files, we found it quite difficult if we have to write these verification code, even though the code generated would not be considered complex.

What's next for Guardrails Atomic

We envision Guardrails Atomic to be a powerful ally of any developers that amalgamates the velocity of AI-driven development and safety of fully verified programs. We hope to integrate it as an AI coding agent of platforms like Claude Code, Gemini and CodeX, so that users need not change their usage patterns and can receive formally verified code from the same source of code.

We hope to optimize the next steps towards developers in areas where program correctness is the most valuable and most vulnerable. Some

We recognize that Guardrails Atomic is currently limited by its ability to serve a diverse user base when it only supports generating TypeScript - we hope to continue pursuing this project by increasing the set of langages supported, for which Z3 is a powerful ally with its cross-language portability.