Show HN: Let formal specs test AI implementations SpecGuardian, a new open-source tool from developer mrasu, generates Go conformance tests from FizzBee formal specifications to check whether an AI-generated implementation reaches only states the spec allows. In the included cache-aside tutorial, SpecGuardian injects an I/O error immediately before cache invalidation and compares the observed state against spec-permitted states; a reordered WriteAndInvalidate that deletes the cache entry before writing to the database fails the test with "actual state does not match any allowed state," leaving the database holding "old" while the cache entry is gone. The example runs with Go and Docker Compose via `go test -count=1 -tags=specguardian ./conformance/...`, with state observation and providers configured in `specguardian.yml`. Let formal specs test AI implementations. A FizzBee https://fizzbee.io/ spec describes the state transitions your system allows. However, the spec does not test whether your implementation follows those transitions. SpecGuardian turns FizzBee's results into tests that check whether your implementation reaches an allowed state. SpecGuardian lets you verify that an AI-generated implementation actually conforms to your specification. In this cache-aside example, a WriteAndInvalidate action stores a new value in the database, then invalidates the corresponding cache entry. The tutorial spec https://github.com/mrasu/spec-guardian/blob/main/examples/tutorial cache aside write/docs/spec/CacheAside.fizz models each operation as atomic and allows a crash before or between them: @conformance role CacheAside: fair action WriteAndInvalidate: Yield to allow a crash before the first I/O. atomic: pass Write to the database first, then invalidate the cache. db.write self.key, self.write value cache.delete cache self.key SpecGuardian generates Go tests https://github.com/mrasu/spec-guardian/blob/main/examples/tutorial cache aside write/conformance/specguardian/cacheaside conformance generated test.go from FizzBee's results. They compare the observed state after the action with states allowed by the spec, including states reached when an I/O operation fails. For example, the generated Go test injects an error into the implementation just before cache invalidation, then checks whether the resulting state is allowed by the spec. Consider an ordering bug in WriteAndInvalidate : cache invalidation runs before the database write. func ca CacheAside WriteAndInvalidate ctx context.Context, input Input Output, error { + if err := ca.cache.Delete ctx, input.Key ; err = nil { + return nil, err + } + if err := ca.db.Write ctx, input.Key, input.Value ; err = nil { return nil, err } - if err := ca.cache.Delete ctx, input.Key ; err = nil { - return nil, err - } - return &Output{Key: input.Key, Value: input.Value}, nil } Both orders produce the same final state on success. But when the database write fails after cache invalidation, the database still holds old value and the cache entry is gone. The spec writes to the database first, so stopping at any point cannot produce this combination. The test fails with the following output excerpt : actual state does not match any allowed state: I/O events: 1. valkey.Do 2. sql.BeginTx fault injected; call not executed The mismatch excerpts show the unchanged database value and missing cache entry: Fields.DB.Records 0 .Value -want +got : string - "new", + "old", Fields.Cache.CachedRecords -want +got : map string string{ - "cached": "old", } To try this example locally, start with the included cache-aside write tutorial. You'll need Go and Docker Compose; the FizzBee exploration results and generated tests are included. Clone the repository and run the example: git clone https://github.com/mrasu/spec-guardian.git cd spec-guardian/examples/tutorial cache aside write docker compose up -d go test -count=1 -tags=specguardian ./conformance/... The test passes, checking normal completion and injected I/O failures. Apply the diff above to cache aside.go and rerun the go test command to reproduce the failure. Restore the original order to make the test pass again. Here's how SpecGuardian works: 1. FizzBee explores the possible states described by the spec. 2. SpecGuardian generates Go tests from the exploration results. 3. Either AI or you write the setup and Action execution code, configure providers in specguardian.yml , and write any remaining state observation code. 4. The tests run a function normally and with an error injected immediately before a supported I/O call, then compare the observed state with states allowed by the spec. specguardian.yml configures state observation and comparison. See the configuration schema https://github.com/mrasu/spec-guardian/blob/main/docs/specguardian.schema.yaml for available settings and the example configuration https://github.com/mrasu/spec-guardian/blob/main/examples/tutorial cache aside write/specguardian.yml for an example. SpecGuardian checks whether an Action ends in a state allowed by the FizzBee spec, including after an injected I/O failure. It complements other tests: - Different from unit tests: It checks the resulting application state against the spec, beyond assertions about individual functions. - Different from integration tests: The expected states come from a FizzBee spec defined independently of the implementation. To generate tests for your project, install FizzBee https://fizzbee.io/ and run these commands from your Go module directory: fizz --output-dir path/to/output dir path/to/YourSpec.fizz go get -tool github.com/mrasu/spec-guardian go tool spec-guardian init --fizzbee-output-dir path/to/output dir Configure observation and comparison. $EDITOR specguardian.yml go generate ./conformance Replace