fastverk

An assurance platform for agent-written code: hermetic builds, blast-radius-scoped tests, and a merge gate that runs every test a change can reach. Its spec substrate pairs an RDF/SPARQL corpus toolkit over Apache Jena with a Lean 4 proof kernel whose trusted axiom base is ratcheted by CI.</summary> <parameter name="story">Speed was never the hard part — trust is. An agent that opens thirty pull requests an hour is a liability until something can prove each one didn't break a test it never thought to run, and fastverk is the layer between "the agent is done" and "it's in main." The platform is assembled from one Bazel module per concern, published to its own bzlmod registry and composed into hermetic builds, with capabilities added as narrowly-scoped gRPC plugins rather than forks of a core. The thesis gets tested on itself in the `spec` repo: an `rfc:` RDF vocabulary with SHACL shapes and 78 SPARQL query files, wired by a `spec_corpus_gates` macro that generates one zero-row gate per consistency invariant — dangling references, dependency cycles, diagnostic-code collisions, asymmetric inverse edges — so that adding a rule needs a query file rather than a code change. Alongside it sits a Lean 4 kernel of seven pillars collapsing a catalogue of 55 spec-level commitments. The sharpest artifact in the repo is `lean/audit_proofs.sh`, which exists because someone measured that `lean_test` does not actually check proofs: a probe theorem proved `by sorry` left the target green. The fix was `set_option warningAsError true` in every source, a ban on `native_decide`, an audit asserting the option cannot be quietly removed, and a ratchet holding the trusted base at its recorded 93 axioms. The same reasoning — that a gate only ever shown to accept is an assertion, not a check — drives an adversarial test that plants a cycle and a dangling reference to prove the consistency gates reject, and a conformance suite whose safety-rule fixtures live in JSON, a language neither the Rust nor the TypeScript implementation is written in, so the two cannot silently diverge.