Matthew Marshall
Passionate and detail-oriented software engineering leader with extensive experience in distributed systems, cloud-native architectures, and finance. Skilled in designing and optimizing high-performance systems, leading engineering teams, and delivering critical enterprise solutions. Proven track record in leading complex technical initiatives, implementing scalable architectures, and driving operational efficiency in fast-paced environments. References available upon request.
Selected work
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.
tomato-bazel
The build plane beneath fastverk: a bzlmod registry publishing 84 modules across 480 versions, a Buildbarn remote-execution cluster modelled as Kubernetes CRDs, and an admission gate that projects the module graph into RDF and enforces invariants as SPARQL queries where the returned rows are the counterexample.</parameter> <parameter name="story">This is what happens when a monorepo is decomposed into a constellation of independently versioned modules and the seams have to be held by machines rather than convention. At the centre is a self-hosted bzlmod registry carrying 84 modules — 56 of them `rules_*` — across 480 published versions, released through a purpose-built Rust CLI that computes source integrity itself. Admission used to be audited by weekly cron, which is how, in the workflow's own words, "135 findings accrued across 300-odd published versions"; it now happens at pull-request time through `gate`, a Rust pipeline that evaluates MODULE.bazel files, runs minimal version selection, projects the resulting facts into Turtle, and runs one SPARQL query per invariant. Ten such gates exist today — unpinned overrides in published modules, atoms selected at multiple versions, toolchain-registration leakage, unnamespaced extension repos, metadata drift — and a gate is one query file plus one target, so adding an invariant needs no Rust rebuild. Because the corpus is not yet clean, the merge check runs as a ratchet rather than a gate: it projects both the pull request and its base, compares per-gate counts, and fails only on regression, which stops things getting worse instead of demanding zero first. The execution side is a Buildbarn cluster expressed as `RbeCluster` and `WorkerPool` custom resources, with a CI action that lets a workflow name only its tenant and receive its endpoint, credential and exec-property flags from the platform at runtime rather than transcribing them. The rulesets themselves are deeper than wrappers: `rules_lean` reuses mathlib's upstream olean cache and adds a test that audits a theorem's transitive axiom set through `Lean.collectAxioms`, catching a dependency that silently introduces `Classical.choice`; `rules_cloudformation` generates roughly 1,582 typed rules, one per AWS resource type, from the pinned upstream schema; `rules_tla` runs TLC model-checking as ordinary `bazel test` targets.
meridian
A server-driven UI framework where an interface is a protobuf message rather than frontend code. One 21-arm PanelDescriptor is authored once and drawn by independent web, React/MUI, and Rust/ratatui renderers, with a shared Rust core compiled to wasm so ranking and validation cannot fork between surfaces.</parameter> <parameter name="story">meridian treats a user interface as data: a single `meridian.ui.v1.PanelDescriptor` — a 21-arm oneof spanning tables, forms, galleries, command palettes, charts, KPI tiles, interactive terminals and append-only log streams — authored once and rendered by surfaces that know nothing about each other. Style, semantics and rendering are deliberately orthogonal proto layers, and the dependency rule runs one way: emitters and renderers depend on the schema module, nothing depends on a renderer. That constraint is what allows a Rust interaction core to be shared verbatim between the browser and a ratatui terminal renderer, compiled to wasm for the former and linked natively for the latter, crossing the boundary as protobuf binary so ranking, validation and dedupe cannot diverge between surfaces. Each panel is documented with a degradation ladder rather than a web-only rendering, so a surface that cannot draw a video shows a poster and then alt text. Two pieces were hard-won. Renderer coverage used to be "only knowable by reading six dispatch sites in four repositories and three languages", so it became a machine-checked manifest — a 21-shape by 6-renderer matrix where every non-rendering cell carries a written reason and adding a proto arm without declaring coverage fails the build. And because the MCP server lets a model author a descriptor, the admission gate derives read-versus-mutation from the renderer callsite rather than from any field on the descriptor, precisely so an untrusted author cannot promote a read into a mutation. The project's most consequential event was folding ten repositories into one workspace: 279 commits preserved, five pairwise-disjoint versions of the generated proto types collapsed to one, and CI added to four repos covering some 14,500 lines that had none — which immediately surfaced a `Block.view` arm that had gone unhandled for four minor releases because nobody could build the TUI.