These functions are just simply three-bit input boolean functions (used bitslice style in SHA2).
With only 8 possible inputs exhaustion is a perfectly valid proof technique:
#include <stdio.h>
#include <stdlib.h>
int CH(int x,int y,int z) { return (x & y) | ((~x) & z); }
int CH_alt(int x,int y,int z) { return z ^ (x & (y ^ z)); }
int MAJ(int x,int y,int z) { return (x & y) ^ (x & z) ^ (y & z);}
int MAJ_alt(int x,int y,int z) { return (x & y) | (z & (x | y));};
int main(void){
int x,y,z;
for (x=0; x<2; x++) {
for (y=0; y<2; y++) {
for (z=0; z<2; z++) {
if((CH(x,y,z) != CH_alt(x,y,z)) || (MAJ(x,y,z) != MAJ_alt(x,y,z))) {
printf("quod est absurdum\n");
exit(1);
}
}
}
}
printf("QED\n");
return 0;
}