Mason Hall
Community@fmhall · New York City, NY
Engineering and strategy @Merit-Systems. Formerly @a16z
Agent Skills by Mason Hall
Showing 18 vetted skills indexed across 1 GitHub repositories.
fmhalllean-array-list
Provide Lean 4 proof strategies and lemmas for ByteArray, Array, and List operations.
fmhalllean-content-preservation
Formally verify content preservation and characterization in Lean 4 buffer operations.
fmhalllean-roundtrip-proofs
Generate roundtrip theorems for Lean 4 PNG encoding and decoding.
fmhallpng-interlace-proofs
Verify Adam7 interlacing properties in PNG images for correct decoding and re-encoding.
fmhalllean-monad-proofs
Optimize Lean 4 proofs involving monads and do-notation.
fmhalllean-parsing-completeness
Generate proof patterns for parsing completeness in Lean code.
fmhalllean-fuel-induction
Automate fuel independence proof verification for Lean 4 recursive functions.
fmhalllean-wf-recursion
Guide constructing well-founded recursion proofs in Lean 4.
fmhallpng-chunk-framing
Verify PNG chunk parsing, serialization, and CRC32 correctness with Lean 4 and lean-zip.
fmhallagent-pr-recovery
Diagnose and resolve merge conflicts and rebase stale branches in PR workflows.
fmhallpng-filter-proofs
Verify PNG scanline filter roundtrip proofs using Lean 4.
fmhallagent-worker-flow
Automate claim, branch, verify, and publish workflows for GitHub issues and pull requests.
fmhallproof-review-checklist
Review Lean 4 proof files for quality, cleanup, and coding standards.
fmhalllean-simp-tactics
Provide Lean 4 tactics for simplifying proofs with simp only failures.
fmhalllean-no-mathlib
Provide Lean 4 tactic alternatives for proofs without Mathlib.
fmhallproven-bounds
Convert runtime bounds checks to proven bounds in Lean 4 code.
fmhalllean-dependent-types
Resolve dependent type issues in Lean 4 with recursion and scoping guidance.
fmhalllean-uint-bitvec
Convert between numeric types and BitVec in Lean 4 proofs.